Support for separation logic. Enable cbqi by default for pure BV.

37 files changed, 609 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 7d7690d22..45842065f 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus sep
 DIST_SUBDIRS = $(SUBDIRS)
 
 # don't override a BINARY imported from a personal.mk
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
new file mode 100644
index 000000000..9d2abaa18
--- /dev/null
+++ b/test/regress/regress0/sep/Makefile.am
@@ -0,0 +1,76 @@
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+  pto-01.smt2 \
+  pto-02.smt2 \
+  pto-04.smt2 \
+  sep-01.smt2 \
+  sep-02.smt2 \
+  sep-03.smt2 \
+  sep-find2.smt2 \
+  sep-neg-nstrict.smt2 \
+  sep-plus1.smt2 \
+  sep-nterm-val-model.smt2 \
+  crash1220.smt2 \
+  nspatial-simp.smt2 \
+  sep-neg-1refine.smt2 \
+  sep-neg-simple.smt2 \
+  sep-simp-unc.smt2 \
+  sep-simp-unsat-emp.smt2 \
+  simple-neg-sat.smt2 \
+  wand-simp-sat.smt2 \
+  wand-simp-sat2.smt2 \
+  wand-simp-unsat.smt2 \
+  sep-nterm-again.smt2 \
+  split-find-unsat.smt2 \
+  split-find-unsat-w-emp.smt2 \
+  nemp.smt2 \
+  wand-crash.smt2 \
+  wand-nterm-simp.smt2 \
+  wand-nterm-simp2.smt2 \
+  loop-1220.smt2 \
+  chain-int.smt2 \
+  sep-neg-swap.smt2 \
+  sep-neg-nstrict2.smt2 \
+  dispose-list-4-init.smt2 \
+  wand-0526-sat.smt2 \
+  quant_wand.smt2 \
+  fmf-nemp-2.smt2
+
+
+FAILING_TESTS =
+# loop-1220.smt2 (slow)
+
+EXTRA_DIST = $(TESTS)
+
+#   slow after changes on Nov 20 : artemis-0512-nonterm.smt2
+#   slow after decision engine respects requirePhase: type003.smt2  loop007.smt2 
+
+# and make sure to distribute it
+EXTRA_DIST +=
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2
new file mode 100644
index 000000000..d3245e33f
--- /dev/null
+++ b/test/regress/regress0/sep/chain-int.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(assert (sep (pto x y) (pto y z)))
+(assert (and (> x 3) (< x 5)))
+(assert (and (> y 3) (< y 5)))
+(check-sat)
diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2
new file mode 100755
index 000000000..a0fc5a187
--- /dev/null
+++ b/test/regress/regress0/sep/crash1220.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const a Int)
+
+(declare-const y Int)
+(declare-const b Int)
+
+(assert (or (pto x a) (sep (pto x a) (pto y b))))
+(assert (or (not (pto x a)) (sep (not (pto x a)) (not (pto y b)))))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2
new file mode 100644
index 000000000..766354cd9
--- /dev/null
+++ b/test/regress/regress0/sep/dispose-list-4-init.smt2
@@ -0,0 +1,36 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+
+(declare-sort Loc 0)
+
+(declare-const w Loc)
+(declare-const u1 Loc)
+(declare-const u2 Loc)
+(declare-const u3 Loc)
+(declare-const nil Loc)
+
+(declare-const w1 Loc)
+(declare-const w2 Loc)
+(declare-const w3 Loc)
+(declare-const w4 Loc)
+
+; allocated (not nil)
+(assert (not (= w nil)))
+(assert (not (= u1 nil)))
+(assert (not (= u2 nil)))
+(assert (not (= u3 nil)))
+(assert (not (= w1 nil)))
+(assert (not (= w2 nil)))
+(assert (not (= w4 nil)))
+
+; from model
+;(assert (= w1 u3))
+;(assert (= w2 u2))
+;(assert (= w3 u1))
+;(assert (= w4 u1))
+
+(assert (sep (pto w u1) (pto u1 u2) (pto u2 u3) (pto u3 nil)))
+(assert (and (sep (sep (pto w4 w1) (pto w1 w2) (pto w2 nil)) (pto w w3)) (sep (pto w w4) true)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2
new file mode 100644
index 000000000..71fe96d71
--- /dev/null
+++ b/test/regress/regress0/sep/fmf-nemp-2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --finite-model-find --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun u1 () U)
+(declare-fun u2 () U)
+(assert (not (= u1 u2)))
+(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1)) (pto x 0)))))
+; satisfiable with heap of size 2, model of U of size 3
+(check-sat)
diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2
new file mode 100644
index 000000000..2981606d8
--- /dev/null
+++ b/test/regress/regress0/sep/loop-1220.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const a Int)
+
+(declare-const y Int)
+(declare-const b Int)
+(declare-const y0 Int)
+(declare-const b0 Int)
+(declare-const y00 Int)
+(declare-const b00 Int)
+
+(assert (or false (sep (pto x a) (or false (sep (pto y b) (or false (sep (pto y0 b0) (pto y00 b00) )))))))
+(assert (not (or false (sep (pto x a) (not (or false (sep (pto y b) (not (or false (sep (pto y0 b0) (not (pto y00 b00)) )))))))))) 
+
+(check-sat)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
new file mode 100644
index 000000000..e1e21dd10
--- /dev/null
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(assert (not (emp 0)))
+(check-sat)
diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2
new file mode 100755
index 000000000..0c93719c9
--- /dev/null
+++ b/test/regress/regress0/sep/nspatial-simp.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun x () Int)
+
+(assert (sep (= x 0) (not (= x 5))))
+
+(declare-fun y () Int)
+(assert (pto y 0))
+(check-sat)
diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2
new file mode 100644
index 000000000..b0dece248
--- /dev/null
+++ b/test/regress/regress0/sep/pto-01.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (and (pto x a) (pto x b)))
+
+(assert (not (= a b)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2
new file mode 100644
index 000000000..f0b6d2dee
--- /dev/null
+++ b/test/regress/regress0/sep/pto-02.smt2
@@ -0,0 +1,25 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+
+(declare-const x Int)
+
+(declare-const a1 Int)
+(declare-const a2 Int)
+(declare-const a3 Int)
+(declare-const a4 Int)
+(declare-const a5 Int)
+(declare-const a6 Int)
+(declare-const a7 Int)
+(declare-const a8 Int)
+(declare-const a9 Int)
+
+(assert (and (pto x a1) (pto x a2) (pto x a3) 
+         (pto x a4) (pto x a5) (pto x a6)
+         (pto x a7) (pto x a8) (pto x a9)
+    )
+)
+
+(assert (not (= a1 a2 a3 a4 a5 a6 a7 a8 a9)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2
new file mode 100644
index 000000000..1734c93bb
--- /dev/null
+++ b/test/regress/regress0/sep/pto-04.smt2
@@ -0,0 +1,36 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x1 Int)
+(declare-const x2 Int)
+(declare-const x3 Int)
+(declare-const x4 Int)
+(declare-const x5 Int)
+(declare-const x6 Int)
+(declare-const x7 Int)
+(declare-const x8 Int)
+(declare-const x9 Int)
+
+(declare-const a1 Int)
+(declare-const a2 Int)
+(declare-const a3 Int)
+(declare-const a4 Int)
+(declare-const a5 Int)
+(declare-const a6 Int)
+(declare-const a7 Int)
+(declare-const a8 Int)
+(declare-const a9 Int)
+
+(assert (and (pto x1 a1) (pto x2 a2) (pto x3 a3) 
+         (pto x4 a4) (pto x5 a5) (pto x6 a6)
+         (pto x7 a7) (pto x8 a8) (pto x9 a9)
+    )
+)
+
+(assert (not (and (= x1 x2 x3 x4 x5 x6 x7 x8 x9) 
+          (= a1 a2 a3 a4 a5 a6 a7 a8 a9)
+       )
+    )
+)
+
+(check-sat)
diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2
new file mode 100644
index 000000000..d71b937fc
--- /dev/null
+++ b/test/regress/regress0/sep/quant_wand.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --cbqi-all
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const u Int)
+
+(assert (emp 0))
+
+(assert 
+(forall ((y Int)) 
+(not (wand (pto u 5) (and (= y 42) (pto u 5))))
+))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2
new file mode 100644
index 000000000..c3330f036
--- /dev/null
+++ b/test/regress/regress0/sep/sep-01.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (sep (pto x a) (pto y b)))
+
+(assert (= x y))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2
new file mode 100644
index 000000000..403bcf077
--- /dev/null
+++ b/test/regress/regress0/sep/sep-02.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+
+(assert (sep (pto x a) (pto y b) (pto z c)))
+
+(assert (or (= x y) (= y z) (= x z)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2
new file mode 100644
index 000000000..427c44b50
--- /dev/null
+++ b/test/regress/regress0/sep/sep-03.smt2
@@ -0,0 +1,17 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (and (sep (pto x a) (or (pto x a) (pto y b)))
+       (sep (pto y b) (or (pto x a) (pto y b)))
+    )
+)
+
+(assert (not (sep (pto x a) (pto y b))))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2
new file mode 100644
index 000000000..26a27eb22
--- /dev/null
+++ b/test/regress/regress0/sep/sep-find2.smt2
@@ -0,0 +1,22 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x1 Int)
+(declare-const x2 Int)
+(declare-const x3 Int)
+(declare-const x4 Int)
+(declare-const x5 Int)
+(declare-const x6 Int)
+(declare-const x7 Int)
+
+(declare-const a1 Int)
+(declare-const a2 Int)
+
+(assert (and 
+(sep (pto x1 a1) (pto x2 a2) (pto x4 a2) (pto x5 a2) (pto x6 a2) (pto x7 a2))
+(sep (pto x1 a1) (pto x3 a2))
+))
+
+(assert (distinct x3 x2 x4 x5 x6 x7))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2
new file mode 100644
index 000000000..8ddbdd05f
--- /dev/null
+++ b/test/regress/regress0/sep/sep-neg-1refine.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (sep (pto x a) (pto y b))))
+(assert (sep (pto x a) (pto z b)))
+
+; sat with model where y != z
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2
new file mode 100644
index 000000000..1a69336a8
--- /dev/null
+++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (sep true (pto x a))))
+(assert (sep (pto x a) (pto z b)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2
new file mode 100644
index 000000000..e71e6a51a
--- /dev/null
+++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (= a b)))
+(assert (not (sep true (pto x b))))
+(assert (sep (pto x a) (pto z b)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2
new file mode 100644
index 000000000..191e7527f
--- /dev/null
+++ b/test/regress/regress0/sep/sep-neg-simple.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (pto x a)))
+(assert (sep (pto x a) (pto z b)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2
new file mode 100644
index 000000000..f89a9c0ac
--- /dev/null
+++ b/test/regress/regress0/sep/sep-neg-swap.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (sep (pto y a) (pto x b))))
+(assert (sep (pto x a) (pto y b)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2
new file mode 100644
index 000000000..9b4afe36a
--- /dev/null
+++ b/test/regress/regress0/sep/sep-nterm-again.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+
+(assert (and
+        (not (sep (not (sep (not (pto x a)) (not (pto y b)))) (pto x a) ))
+        (sep (pto x a) (pto y b))
+        )
+)
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2
new file mode 100644
index 000000000..0178134cb
--- /dev/null
+++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2
@@ -0,0 +1,17 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (and 
+  (not (sep (not (pto x a)) (not (pto y b)) ))
+  (sep (pto x (+ a 1)) (pto y (+ b 1)))
+  )
+)
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2
new file mode 100644
index 000000000..772acd981
--- /dev/null
+++ b/test/regress/regress0/sep/sep-plus1.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+
+(assert (and
+        (sep (pto x a) true)
+        (sep (pto y (+ a 1)) true)
+))
+(assert (= x y))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2
new file mode 100755
index 000000000..6cdf51294
--- /dev/null
+++ b/test/regress/regress0/sep/sep-simp-unc.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(declare-fun a () U)
+(declare-fun b () U)
+
+(assert (not (sep (not (pto x a)) (pto y b))))
+(check-sat)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
new file mode 100644
index 000000000..fb58b9d10
--- /dev/null
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(declare-fun a () U)
+(declare-fun b () U)
+
+(assert (emp x))
+(assert (sep (pto x a) (pto y b)))
+(check-sat)
diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2
new file mode 100644
index 000000000..0c0b6a9a3
--- /dev/null
+++ b/test/regress/regress0/sep/simple-neg-sat.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+
+(assert (and
+        (not (sep (not (pto x a)) (pto y b) ))  
+        (sep (pto x a) (pto y b))
+  )
+)
+
+(check-sat)
diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
new file mode 100644
index 000000000..ed3187a96
--- /dev/null
+++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+
+(assert (and
+        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x)) ))
+        (sep (pto x a) (pto y b))
+  )
+)
+
+(check-sat)
diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2
new file mode 100644
index 000000000..54530cbf4
--- /dev/null
+++ b/test/regress/regress0/sep/split-find-unsat.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Int)
+
+(assert (and
+        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) ))
+        (sep (pto x a) (pto y b))
+  )
+)
+
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2
new file mode 100644
index 000000000..0c0ee72ad
--- /dev/null
+++ b/test/regress/regress0/sep/wand-0526-sat.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+(assert (wand (pto x u) (pto y v)))
+(assert (emp 0))
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
new file mode 100644
index 000000000..9b4871323
--- /dev/null
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(assert (wand (emp 0) (emp 0)))
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2
new file mode 100644
index 000000000..e8ee4252c
--- /dev/null
+++ b/test/regress/regress0/sep/wand-nterm-simp.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-fun x () Int)
+(assert (wand (emp x) (pto x 3)))
+(check-sat)
+
diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2
new file mode 100644
index 000000000..69305e95c
--- /dev/null
+++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-fun x () Int)
+(assert (wand (pto x 1) (emp x)))
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2
new file mode 100755
index 000000000..df4bfa6d8
--- /dev/null
+++ b/test/regress/regress0/sep/wand-simp-sat.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-fun x () Int)
+(assert (wand (pto x 1) (pto x 1)))
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2
new file mode 100755
index 000000000..ebc115fdd
--- /dev/null
+++ b/test/regress/regress0/sep/wand-simp-sat2.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-fun x () Int)
+(assert (wand (pto x 1) (pto x 3)))
+(check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2
new file mode 100755
index 000000000..95bc85537
--- /dev/null
+++ b/test/regress/regress0/sep/wand-simp-unsat.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-fun x () Int)
+(assert (wand (pto x 1) (pto x 3)))
+(assert (emp x))
+(check-sat)