From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Tue, 1 Dec 2020 15:08:07 +0000 (+0100)
Subject: Add regressions from #5099 (#5557)
X-Git-Tag: cvc5-1.0.0~2534
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75359f120b1cdfa77add48ef11c776f530783c31;p=cvc5.git

Add regressions from #5099 (#5557)

The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions.
Closes #5099.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6c064833a..1a2451147 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -585,6 +585,8 @@ set(regress_0_tests
   regress0/issue4010-sort-inf-var.smt2
   regress0/issue4469-unc-no-reuse-var.smt2
   regress0/issue4707-bv-to-bool-small.smt2
+  regress0/issue5099-model-1.smt2
+  regress0/issue5099-model-2.smt2
   regress0/issue5144-resetAssertions.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
diff --git a/test/regress/regress0/issue5099-model-1.smt2 b/test/regress/regress0/issue5099-model-1.smt2
new file mode 100644
index 000000000..dd422ab3b
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((baz true))
+(set-logic QF_NIRA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (! (or (= a (div 0 b))) :named baz))
+(assert (and (> b 5)))
+(check-sat)
+(get-assignment)
diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2
new file mode 100644
index 000000000..2bd27093f
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((IP true))
+(set-logic QF_NRA)
+(declare-const r11 Real)
+(declare-const r16 Real)
+(assert (! (distinct (/ 1 r16) r11) :named IP))
+(check-sat)
+(get-assignment)
\ No newline at end of file