diff options
Diffstat (limited to 'test/regress/regress0/sep')
-rw-r--r-- | test/regress/regress0/sep/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sep/loop-1220.smt2 | 19 | ||||
-rwxr-xr-x | test/regress/regress0/sep/sep-simp-unc.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress0/sep/split-find-unsat-w-emp.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/sep/split-find-unsat.smt2 | 20 |
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) |