diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-06-02 11:18:36 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-02 11:18:36 -0700 |
| commit | d440c5f3bea930c4f30d62858b878ab36c676312 (patch) | |
| tree | b2a0b76a76c99902814b0a2c6ae4dd3b98d37f57 /test | |
| parent | 806f4071423ee1bf8f02f1836843de73faabb952 (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.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv-abstr-bug2.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0e0cee7f8..0c5920951 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -161,6 +161,7 @@ REG0_TESTS = \ regress0/bv/bug733.smt2 \ regress0/bv/bug734.smt2 \ regress0/bv/bv-abstr-bug.smt2 \ + regress0/bv/bv-abstr-bug2.smt2 \ regress0/bv/bv-int-collapse1.smt2 \ regress0/bv/bv-int-collapse2.smt2 \ regress0/bv/bv-options1.smt2 \ diff --git a/test/regress/regress0/bv/bv-abstr-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2 new file mode 100644 index 000000000..939439adf --- /dev/null +++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager +(set-logic QF_NIA) +(set-info :status sat) +(declare-fun _substvar_7_ () Bool) +(declare-fun _substvar_3_ () Int) +(assert (or _substvar_7_ (= 0 _substvar_3_))) +(check-sat) |