diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-12 10:21:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-12 10:21:14 -0700 |
commit | ff8beb0b93ca561a3488edca5d06fa7acbbacee2 (patch) | |
tree | 65fe42309de6b86dd4d15a3715047c277ddaaefe /test/regress/regress0/cores | |
parent | 03ad2ad78bee38c30b13af2cc642285d55c77f16 (diff) | |
parent | b71bf740b517c3a530d92c33bd24769330708d76 (diff) |
Merge branch 'master' into mkExceptionPublicmkExceptionPublic
Diffstat (limited to 'test/regress/regress0/cores')
-rw-r--r-- | test/regress/regress0/cores/issue4971-0.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/cores/issue4971-1.smt2 | 1 |
2 files changed, 4 insertions, 3 deletions
diff --git a/test/regress/regress0/cores/issue4971-0.smt2 b/test/regress/regress0/cores/issue4971-0.smt2 index 75878183c..16fdc2b77 100644 --- a/test/regress/regress0/cores/issue4971-0.smt2 +++ b/test/regress/regress0/cores/issue4971-0.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --incremental -q --check-unsat-cores -; EXPECT: unknown +; COMMAND-LINE: --incremental -q --check-unsat-cores --cegqi-full +; EXPECT: unsat ; EXPECT: unsat ; EXPECT: ( ; EXPECT: IP_1 @@ -15,4 +15,4 @@ (assert (! (or (< (abs 404) i4) v14 v1) :named IP_51)) (check-sat) (check-sat-assuming (IP_33 IP_51)) -(get-unsat-core)
\ No newline at end of file +(get-unsat-core) diff --git a/test/regress/regress0/cores/issue4971-1.smt2 b/test/regress/regress0/cores/issue4971-1.smt2 index 9bb4f3e84..2ac70735c 100644 --- a/test/regress/regress0/cores/issue4971-1.smt2 +++ b/test/regress/regress0/cores/issue4971-1.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --incremental -q --check-unsat-cores ; COMMAND-LINE: --incremental -q --check-unsat-cores --unsat-cores-mode=sat-proof ; EXPECT: sat ; EXPECT: sat |