From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Oct 2021 21:12:09 +0000 (-0500)
Subject: Add regression for fixed issue (#7365)
X-Git-Tag: cvc5-1.0.0~1064
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4affc8f76d443e453de62151979567e702da431e;p=cvc5.git

Add regression for fixed issue (#7365)

Fixes #6845.

This issue does not occur in current master.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 79a493a1f..baced1e76 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1902,6 +1902,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
   regress1/quantifiers/issue5899-qe.smt2
   regress1/quantifiers/issue6699-nc-shadow.smt2
+  regress1/quantifiers/issue6845-nl-lemma-tc.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2
new file mode 100644
index 000000000..087137653
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic NIRA)
+(declare-const x Bool)
+(declare-fun i () Int)
+(declare-fun i1 () Int)
+(assert (< 1.0 (to_real i)))
+(assert (distinct 0 (/ 7 (to_real i))))
+(push)
+(assert (or (exists ((q Int)) (= 0 (* i i1)))))
+(check-sat)
+(pop)
+(assert (or (= i1 1) x))
+(check-sat)