summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sep
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sep')
-rw-r--r--test/regress/regress0/sep/Makefile.am3
-rw-r--r--test/regress/regress0/sep/dup-nemp.smt27
2 files changed, 9 insertions, 1 deletions
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index d72e02d97..6078bfa19 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -55,7 +55,8 @@ TESTS = \
quant_wand.smt2 \
fmf-nemp-2.smt2 \
trees-1.smt2 \
- wand-false.smt2
+ wand-false.smt2 \
+ dup-nemp.smt2
FAILING_TESTS =
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
new file mode 100644
index 000000000..009561128
--- /dev/null
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(declare-const l Loc)
+(assert (sep (not (emp l)) (not (emp l))))
+(assert (pto l l))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback