diff options
| author | guykatzz <katz911@gmail.com> | 2017-03-17 14:11:41 -0700 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2017-03-17 14:12:04 -0700 |
| commit | 768534c0973788cab0097c6485e5113da1d406da (patch) | |
| tree | 32e8eda1c7882f05b16c4bbec4e4095efbec34d3 /test/regress/regress0/arrays | |
| parent | afe84522b87b6fc0ad5d0e9a396b61f7b523f674 (diff) | |
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
Diffstat (limited to 'test/regress/regress0/arrays')
| -rw-r--r-- | test/regress/regress0/arrays/bool-array.smt2 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test/regress/regress0/arrays/bool-array.smt2 b/test/regress/regress0/arrays/bool-array.smt2 index f05d0266b..0e5920384 100644 --- a/test/regress/regress0/arrays/bool-array.smt2 +++ b/test/regress/regress0/arrays/bool-array.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_AX) (set-info :status unsat) @@ -10,4 +9,3 @@ (assert (= (select a true) (select a false))) (check-sat) - |