diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-12-01 16:08:07 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-01 16:08:07 +0100 |
| commit | 75359f120b1cdfa77add48ef11c776f530783c31 (patch) | |
| tree | 8293b4d7d30abf4c3078334401bc95c0625db31e | |
| parent | 7fb5354114c7e17260b3ff520decf340734d52fe (diff) | |
Add regressions from #5099 (#5557)
The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions.
Closes #5099.
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/issue5099-model-1.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress0/issue5099-model-2.smt2 | 9 |
3 files changed, 21 insertions, 0 deletions
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 |