diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-09 11:49:35 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-09 11:49:35 -0700 |
| commit | 70a96669c694c41be7119bbeaf50c68bdf59ffef (patch) | |
| tree | 6639c1c4b00fdf7e4e3485d84a4e40691252a035 | |
| parent | b2c4184f1148ba1c51011ee6dd8341b9f204f54e (diff) | |
Make regression test `issue4971-0` more robustfixRegression4971
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) |