From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Jul 2020 18:08:45 +0000 (-0500)
Subject: Fix regression output. (#4741)
X-Git-Tag: cvc5-1.0.0~3110
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=455fed0b388ff9c534391eb88f8c2a336fa42f07;p=cvc5.git

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