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.

diff --git a/test/regress/regress0/cores/issue4971-0.smt2 b/test/regress/regress0/cores/issue4971-0.smt2
index 75878183cf7bc24d8d2ce7a98428457fa2bbd5b1..16fdc2b7756fe07b97751f2a784f3f6448a97ba5 100644 (file)
--- 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)