From 75359f120b1cdfa77add48ef11c776f530783c31 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 16:08:07 +0100 Subject: [PATCH] Add regressions from #5099 (#5557) The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions. Closes #5099. --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/issue5099-model-1.smt2 | 10 ++++++++++ test/regress/regress0/issue5099-model-2.smt2 | 9 +++++++++ 3 files changed, 21 insertions(+) create mode 100644 test/regress/regress0/issue5099-model-1.smt2 create mode 100644 test/regress/regress0/issue5099-model-2.smt2 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 -- 2.30.2