diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-09 12:15:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-09 14:15:51 -0500 |
| commit | e7c06200748ca209a52ecf1f73bff3e51ebfdb99 (patch) | |
| tree | 6639c1c4b00fdf7e4e3485d84a4e40691252a035 | |
| parent | b2c4184f1148ba1c51011ee6dd8341b9f204f54e (diff) | |
Make regression test `issue4971-0` more robust (#6857)
When compiling and running cvc5 on macOS with an M1 CPU, the regression
test regress0/cores/issue4971-0.smt2 returned unsat instead of the
expected unknown for the first (check-sat) command. This commit
makes the regression more robust by adding --cegqi-full and expecting
unsat.
| -rw-r--r-- | test/regress/regress0/cores/issue4971-0.smt2 | 6 |
1 files changed, 3 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) |