diff options
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) |