From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 9 Jul 2021 19:15:51 +0000 (-0700)
Subject: Make regression test `issue4971-0` more robust (#6857)
X-Git-Tag: cvc5-1.0.0~1509
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7c06200748ca209a52ecf1f73bff3e51ebfdb99;p=cvc5.git

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 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)