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/regress0/sep | |
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/regress0/sep')
-rw-r--r-- | test/regress/regress0/sep/issue5343-err.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
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) |