Move slow regress0 benchmarks to regress1, increment regress1 through regress3.

5 files changed, 0 insertions, 73 deletions

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index b43a9a570..d7bfa2d57 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -33,20 +33,16 @@ TESTS =	\
   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 \
diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2
deleted file mode 100644
index b857aec2a..000000000
--- a/test/regress/regress0/sep/loop-1220.smt2
+++ /dev/null
@@ -1,19 +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)
-(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/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2
deleted file mode 100755
index cedbb53eb..000000000
--- a/test/regress/regress0/sep/sep-simp-unc.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-(set-logic QF_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/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
deleted file mode 100644
index 10e509e05..000000000
--- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
+++ /dev/null
@@ -1,18 +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 (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
deleted file mode 100644
index 1a9e76a8a..000000000
--- a/test/regress/regress0/sep/split-find-unsat.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: unsat
-(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 (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)