diff options
Diffstat (limited to 'test/regress/regress0/smtlib/set-info-status.smt2')
| -rw-r--r-- | test/regress/regress0/smtlib/set-info-status.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/smtlib/set-info-status.smt2 b/test/regress/regress0/smtlib/set-info-status.smt2 new file mode 100644 index 000000000..489d686b3 --- /dev/null +++ b/test/regress/regress0/smtlib/set-info-status.smt2 @@ -0,0 +1,22 @@ +; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +; EXPECT-ERROR: Expected result unsat but got sat +; ERROR-SCRUBBER: sed -e '/Fatal failure within.*/d' +; EXIT: -6 +(set-option :incremental true) +(set-option :produce-unsat-cores true) +(set-logic QF_BV) +(set-info :status unsat) +(get-unsat-core) +(set-info :status sat) +(check-sat) +(set-info :status sat) +(check-sat) +(push) +(assert false) +(check-sat) +(pop) +(set-info :status unsat) +(check-sat) |