diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-09-29 16:32:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-29 21:32:31 +0000 |
| commit | bed236463f34019a802c8f0ee66f386b77ac4446 (patch) | |
| tree | b243c34aa9382f34f87c187ae136c000ac2d906e /test/regress/regress0 | |
| parent | 7d859b19c2755dc5071f4bedbbeab8a37870e69a (diff) | |
Remove support for extended `(check-sat <term>)` command. (#7270)
This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/cores/issue4925.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue5238.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue5902.smt2 | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress0/cores/issue4925.smt2 b/test/regress/regress0/cores/issue4925.smt2 index 951f7e008..62428b565 100644 --- a/test/regress/regress0/cores/issue4925.smt2 +++ b/test/regress/regress0/cores/issue4925.smt2 @@ -12,5 +12,5 @@ (assert (or (< a 1) (> c 1))) (check-sat) (assert (= b (- 1))) -(check-sat true) -(check-sat)
\ No newline at end of file +(check-sat-assuming (true)) +(check-sat) diff --git a/test/regress/regress0/cores/issue5238.smt2 b/test/regress/regress0/cores/issue5238.smt2 index ae3bed2e2..faf72f0e1 100644 --- a/test/regress/regress0/cores/issue5238.smt2 +++ b/test/regress/regress0/cores/issue5238.smt2 @@ -10,5 +10,5 @@ (assert (= (/ 0 a) 1)) (check-sat) (assert (= (+ a b) 0)) -(check-sat (> b 1)) -(check-sat)
\ No newline at end of file +(check-sat-assuming ((> b 1))) +(check-sat) diff --git a/test/regress/regress0/cores/issue5902.smt2 b/test/regress/regress0/cores/issue5902.smt2 index 809873003..3c930b26b 100644 --- a/test/regress/regress0/cores/issue5902.smt2 +++ b/test/regress/regress0/cores/issue5902.smt2 @@ -1,3 +1,3 @@ ; COMMAND-LINE: -q ; EXPECT: unsat -(check-sat false) +(check-sat-assuming (false)) |