From 455fed0b388ff9c534391eb88f8c2a336fa42f07 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Jul 2020 13:08:45 -0500 Subject: [PATCH] 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. --- test/regress/regress1/quantifiers/qid-debug-inst.smt2 | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2 index 6b987a3a3..d7ce3771b 100644 --- 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) -- 2.30.2