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 79a493a1fe1fceefccf4d0aeccd05b007eee40ec..baced1e76740687e88177d160aa379f0da30621a 100644 (file)
--- 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 (file)
index 0000000..0871376
--- /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)