diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-10 20:27:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-10 20:27:38 -0600 |
| commit | 59d8647b04f86421949390a3e958ffdf0df07665 (patch) | |
| tree | a916fa77cb38bb24da805b8e444c3584931652c8 /test/regress | |
| parent | e0009c822488a2c39f8907e37333409c1191d47b (diff) | |
Fix preregistration in TheorySep before declare-heap (#5411)
Followup to fix for #5343. This catches cases where separation logic constraints are preregistered to TheorySep before the heap has been declared, which should also result in an error.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sep/issue5343-err.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9a0565d8e..ac62452e5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -869,6 +869,7 @@ set(regress_0_tests regress0/sep/dispose-1.smt2 regress0/sep/dup-nemp.smt2 regress0/sep/issue3720-check-model.smt2 + regress0/sep/issue5343-err.smt2 regress0/sep/nemp.smt2 regress0/sep/nil-no-elim.smt2 regress0/sep/nspatial-simp.smt2 diff --git a/test/regress/regress0/sep/issue5343-err.smt2 b/test/regress/regress0/sep/issue5343-err.smt2 new file mode 100644 index 000000000..ea37815fa --- /dev/null +++ b/test/regress/regress0/sep/issue5343-err.smt2 @@ -0,0 +1,8 @@ +; REQUIRES: no-competition +; COMMAND-LINE: +; EXPECT: (error "ERROR: the type of the separation logic heap has not been declared (e.g. via a declare-heap command), and we have a separation logic constraint (wand true true) +; EXPECT: ") +; EXIT: 1 +(set-logic QF_ALL_SUPPORTED) +(assert (wand true true)) +(check-sat) |