From e7c06200748ca209a52ecf1f73bff3e51ebfdb99 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 9 Jul 2021 12:15:51 -0700 Subject: [PATCH] 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. --- test/regress/regress0/cores/issue4971-0.smt2 | 6 +++--- 1 file 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) -- 2.30.2