Refactor regressions (#1581)

28 files changed, 0 insertions, 431 deletions

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 692390dde..9b6c44fa5 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -21,42 +21,15 @@ MAKEFLAGS = -k
 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-unsat-emp.smt2 \
-  simple-neg-sat.smt2 \
-  wand-simp-sat.smt2 \
-  wand-simp-sat2.smt2 \
-  wand-simp-unsat.smt2 \
-  sep-nterm-again.smt2 \
   nemp.smt2 \
   wand-crash.smt2 \
-  wand-nterm-simp.smt2 \
-  wand-nterm-simp2.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 \
   trees-1.smt2 \
-  wand-false.smt2 \
   dup-nemp.smt2 \
-  emp2-quant-unsat.smt2 \
   dispose-1.smt2 \
-  finite-witness-sat.smt2 \
-  sep-fmf-priority.smt2 \
   nil-no-elim.smt2
 
 
diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2
deleted file mode 100644
index ebe52fa46..000000000
--- a/test/regress/regress0/sep/chain-int.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-(set-logic QF_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
deleted file mode 100644
index f68434f33..000000000
--- a/test/regress/regress0/sep/crash1220.smt2
+++ /dev/null
@@ -1,15 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index b3e2088b1..000000000
--- a/test/regress/regress0/sep/dispose-list-4-init.smt2
+++ /dev/null
@@ -1,36 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2
deleted file mode 100644
index e89c0fd30..000000000
--- a/test/regress/regress0/sep/emp2-quant-unsat.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-; COMMAND-LINE: --quant-epr
-; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
-(set-info :status unsat)
-(declare-sort U 0)
-(declare-fun u () U)
-
-(assert (sep (not (emp u u)) (not (emp u u))))
-
-(assert (forall ((x U) (y U)) (= x y)))
-
-(check-sat)
diff --git a/test/regress/regress0/sep/finite-witness-sat.smt2 b/test/regress/regress0/sep/finite-witness-sat.smt2
deleted file mode 100644
index 8aedbfd25..000000000
--- a/test/regress/regress0/sep/finite-witness-sat.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models
-; EXPECT: sat
-(set-logic ALL_SUPPORTED)
-(declare-sort Loc 0)
-(declare-const l Loc)
-
-(assert (not (emp l l)))
-(assert (forall ((x Loc) (y Loc)) (not (pto x y))))
-
-
-(check-sat)
diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2
deleted file mode 100644
index 679b1e363..000000000
--- a/test/regress/regress0/sep/fmf-nemp-2.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; 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 0)) (pto x 0)))))
-; satisfiable with heap of size 2, model of U of size 3
-(check-sat)
diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2
deleted file mode 100644
index 9b0afda7a..000000000
--- a/test/regress/regress0/sep/pto-04.smt2
+++ /dev/null
@@ -1,36 +0,0 @@
-(set-logic QF_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
deleted file mode 100644
index 8a69c10c4..000000000
--- a/test/regress/regress0/sep/quant_wand.smt2
+++ /dev/null
@@ -1,15 +0,0 @@
-; COMMAND-LINE: --full-saturate-quant
-; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
-(set-info :status unsat)
-
-(declare-const u Int)
-
-(assert (emp 0 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-02.smt2 b/test/regress/regress0/sep/sep-02.smt2
deleted file mode 100644
index 6f190d964..000000000
--- a/test/regress/regress0/sep/sep-02.smt2
+++ /dev/null
@@ -1,16 +0,0 @@
-(set-logic QF_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
deleted file mode 100644
index 8dce5acc7..000000000
--- a/test/regress/regress0/sep/sep-03.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-(set-logic QF_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
deleted file mode 100644
index 356f866c1..000000000
--- a/test/regress/regress0/sep/sep-find2.smt2
+++ /dev/null
@@ -1,22 +0,0 @@
-(set-logic QF_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-fmf-priority.smt2 b/test/regress/regress0/sep/sep-fmf-priority.smt2
deleted file mode 100644
index fe3af1b35..000000000
--- a/test/regress/regress0/sep/sep-fmf-priority.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models
-; EXPECT: sat
-(set-logic ALL_SUPPORTED)
-
-(declare-sort Loc 0)
-(declare-const l Loc)
-(declare-const x Loc)
-
-(assert (wand (pto x x) false))
-(assert (forall ((x Loc) (y Loc)) (not (pto x y))))
-
-(check-sat)
diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2
deleted file mode 100644
index ab12c6461..000000000
--- a/test/regress/regress0/sep/sep-neg-1refine.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index 425e5ce3c..000000000
--- a/test/regress/regress0/sep/sep-neg-nstrict.smt2
+++ /dev/null
@@ -1,15 +0,0 @@
-(set-logic QF_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
deleted file mode 100644
index 7ada6ff06..000000000
--- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2
+++ /dev/null
@@ -1,18 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index 7b6fc69e9..000000000
--- a/test/regress/regress0/sep/sep-neg-simple.smt2
+++ /dev/null
@@ -1,16 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index 53f890b0d..000000000
--- a/test/regress/regress0/sep/sep-neg-swap.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index 3e595b5e9..000000000
--- a/test/regress/regress0/sep/sep-nterm-again.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index d4fb0fd52..000000000
--- a/test/regress/regress0/sep/sep-nterm-val-model.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-(set-logic QF_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/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2
deleted file mode 100644
index 70927ad82..000000000
--- a/test/regress/regress0/sep/simple-neg-sat.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2
deleted file mode 100644
index 12aa0a67e..000000000
--- a/test/regress/regress0/sep/wand-0526-sat.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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 0))
-(check-sat)
diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2
deleted file mode 100644
index 65500f775..000000000
--- a/test/regress/regress0/sep/wand-false.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
-(set-info :status sat)
-(declare-fun x () Int)
-(assert (wand (pto x x) false))
-(check-sat)
diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2
deleted file mode 100644
index b59b53b58..000000000
--- a/test/regress/regress0/sep/wand-nterm-simp.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
-(declare-fun x () Int)
-(assert (wand (emp x 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
deleted file mode 100644
index fa6a83143..000000000
--- a/test/regress/regress0/sep/wand-nterm-simp2.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
-(set-info :status sat)
-(declare-fun x () Int)
-(assert (wand (pto x 1) (emp x x)))
-(check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2
deleted file mode 100644
index 120683f74..000000000
--- a/test/regress/regress0/sep/wand-simp-sat.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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
deleted file mode 100644
index c684d16ad..000000000
--- a/test/regress/regress0/sep/wand-simp-sat2.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
-(set-info :status sat)
-(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
deleted file mode 100644
index 850be7b97..000000000
--- a/test/regress/regress0/sep/wand-simp-unsat.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: unsat
-(set-logic QF_ALL_SUPPORTED)
-(declare-fun x () Int)
-(assert (wand (pto x 1) (pto x 3)))
-(assert (emp x x))
-(check-sat)