diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-26 17:02:16 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-26 10:02:16 -0600 |
| commit | 865d1ee48de8e4a21d1e97c707be46c34918367d (patch) | |
| tree | d1721f2cd0ccee285d8a4828cd6c184e2c446046 /test/regress | |
| parent | d3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88 (diff) | |
Make CAD solver work for empty set of assertions (#5535)
When called with no assertions, the CAD solver would still go to work and then segfault when trying to access the first variable.
This PR adds an explicit check for this case and adds a regression.
Fixes #5534 .
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/nl/issue5534-no-assertions.smt2 | 12 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8969b6c01..816202fa9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -622,6 +622,7 @@ set(regress_0_tests regress0/nl/issue3971.smt2 regress0/nl/issue3991.smt2 regress0/nl/issue4007-rint-uf.smt2 + regress0/nl/issue5534-no-assertions.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 diff --git a/test/regress/regress0/nl/issue5534-no-assertions.smt2 b/test/regress/regress0/nl/issue5534-no-assertions.smt2 new file mode 100644 index 000000000..e7a9f0cd1 --- /dev/null +++ b/test/regress/regress0/nl/issue5534-no-assertions.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +(set-logic QF_UFNRA) +(declare-fun r () Real) +(declare-fun u (Real Real) Bool) +(assert (u 0.0 (* r r))) +(push) +(assert (and (< r 0.0) (< 0.0 r))) +(check-sat) +(pop) +(check-sat)
\ No newline at end of file |