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 6c064833a5c7269a02e799e8235e575b4ad1cabe..1a245114708cc61b19f34e760c3a17473e21ef31 100644 (file)
--- 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 (file)
index 0000000..dd422ab
--- /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 (file)
index 0000000..2bd2709
--- /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