Fix regression output. (#4741)

This regression output was unexpected previously since conflict-based instantiation caught a conflict early, this makes it so that the output of this regression should be deterministic.

Fixes regress1.

diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
index 6b987a3a32591a969ad4d63b1b3275abd6cd6203..d7ce3771be687b518d74cabb7a5af4c62e2ace9c 100644 (file)
--- a/test/regress/regress1/quantifiers/qid-debug-inst.smt2
+++ b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
@@ -5,9 +5,10 @@
 
 (set-logic UFLIA)
 (declare-fun P (Int) Bool)
+(declare-fun R (Int) Bool)
 (declare-fun Q (Int) Bool)
-(assert (forall ((x Int)) (! (P x) :qid |myQuant1|)))
+(assert (forall ((x Int)) (! (=> (R x) (P x)) :qid |myQuant1|)))
 (assert (forall ((x Int)) (! (=> (P x) (Q x)) :qid |myQuant2|)))
-(assert (P 5))
+(assert (R 5))
 (assert (not (Q 5)))
 (check-sat)