diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/sep/dispose-1.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/dup-nemp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/emp2-quant-unsat.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/finite-witness-sat.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/fmf-nemp-2.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/nemp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/quant_wand.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/sep-simp-unsat-emp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/trees-1.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/sep/wand-0526-sat.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/wand-crash.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/wand-nterm-simp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sep/wand-nterm-simp2.smt2 | 2 | ||||
-rwxr-xr-x | test/regress/regress0/sep/wand-simp-unsat.smt2 | 2 |
14 files changed, 17 insertions, 15 deletions
diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 index 3c0e7df32..3f908c3be 100644 --- a/test/regress/regress0/sep/dispose-1.smt2 +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -11,7 +11,7 @@ ;----------------- (assert (pto w (as sep.nil Int))) -(assert (not (and (sep (and (emp 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) +(assert (not (and (sep (and (emp 0 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) (check-sat) ;(get-model) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 98348f617..17750eaa3 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -2,6 +2,6 @@ (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) -(assert (sep (not (emp l)) (not (emp l)))) +(assert (sep (not (emp l l)) (not (emp l l)))) (assert (pto l l)) (check-sat) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 index 52d99d8c0..e89c0fd30 100644 --- a/test/regress/regress0/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2 @@ -5,7 +5,7 @@ (declare-sort U 0) (declare-fun u () U) -(assert (sep (not (emp u)) (not (emp u)))) +(assert (sep (not (emp u u)) (not (emp u u)))) (assert (forall ((x U) (y U)) (= x y))) diff --git a/test/regress/regress0/sep/finite-witness-sat.smt2 b/test/regress/regress0/sep/finite-witness-sat.smt2 index 93413d950..8aedbfd25 100644 --- a/test/regress/regress0/sep/finite-witness-sat.smt2 +++ b/test/regress/regress0/sep/finite-witness-sat.smt2 @@ -4,7 +4,7 @@ (declare-sort Loc 0) (declare-const l Loc) -(assert (not (emp l))) +(assert (not (emp l l))) (assert (forall ((x Loc) (y Loc)) (not (pto x y)))) diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2 index 71fe96d71..679b1e363 100644 --- a/test/regress/regress0/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress0/sep/fmf-nemp-2.smt2 @@ -5,6 +5,6 @@ (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))))) +(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/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index a0766a7e0..99d7f9c91 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) -(assert (not (emp 0))) +(assert (not (emp 0 0))) (check-sat) diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2 index d71b937fc..9c38fb405 100644 --- a/test/regress/regress0/sep/quant_wand.smt2 +++ b/test/regress/regress0/sep/quant_wand.smt2 @@ -5,7 +5,7 @@ (declare-const u Int) -(assert (emp 0)) +(assert (emp 0 0)) (assert (forall ((y Int)) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index 9239fb770..42efae553 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -7,6 +7,6 @@ (declare-fun a () U) (declare-fun b () U) -(assert (emp x)) +(assert (emp x x)) (assert (sep (pto x a) (pto y b))) (check-sat) diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 index 8a46d9fdd..3fa0d0555 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -6,6 +6,8 @@ (declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc))))) +(declare-fun data0 () Node) + (declare-const dv Int) (declare-const v Loc) @@ -15,7 +17,7 @@ (declare-const r Loc) (define-fun ten-tree0 ((x Loc) (d Int)) Bool -(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) +(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0 data0) (= l (as sep.nil Loc))) (and (emp loc0 data0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) (declare-const dy Int) (declare-const y Loc) @@ -23,7 +25,7 @@ (declare-const z Loc) (define-fun ord-tree0 ((x Loc) (d Int)) Bool -(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz)))) +(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0 data0) (= y (as sep.nil Loc))) (and (emp loc0 data0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz)))) ;------- f ------- (assert (= y (as sep.nil Loc))) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 index fa0aab591..12aa0a67e 100644 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -6,5 +6,5 @@ (declare-fun u () Int) (declare-fun v () Int) (assert (wand (pto x u) (pto y v))) -(assert (emp 0)) +(assert (emp 0 0)) (check-sat) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 1d799c8c9..dad089f8b 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) -(assert (wand (emp 0) (emp 0))) +(assert (wand (emp 0 0) (emp 0 0))) (check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 index 0db7330d1..b59b53b58 100644 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -2,6 +2,6 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) -(assert (wand (emp x) (pto x 3))) +(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 index cce0f79e3..fa6a83143 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -3,5 +3,5 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) -(assert (wand (pto x 1) (emp x))) +(assert (wand (pto x 1) (emp x x))) (check-sat) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 index c9851661a..850be7b97 100755 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -3,5 +3,5 @@ (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) -(assert (emp x)) +(assert (emp x x)) (check-sat) |