projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 806f407) | patch
Fix BV-abstraction check to consider SKOLEM. (#2042)
authorMathias Preiner <mathias.preiner@gmail.com>
Sat, 2 Jun 2018 18:18:36 +0000 (11:18 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sat, 2 Jun 2018 18:18:36 +0000 (11:18 -0700)
commitd440c5f3bea930c4f30d62858b878ab36c676312
treeb2a0b76a76c99902814b0a2c6ae4dd3b98d37f57tree
parent806f4071423ee1bf8f02f1836843de73faabb952commit | diff
Fix BV-abstraction check to consider SKOLEM. (#2042)

Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.
src/theory/bv/abstraction.cpp diff | blob | history
src/theory/bv/bitblast/aig_bitblaster.cpp diff | blob | history
src/theory/bv/bitblast/aig_bitblaster.h diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress0/bv/bv-abstr-bug2.smt2 [new file with mode: 0644] blob