diff options
Diffstat (limited to 'test/regress/regress1/sep/dispose-list-4-init.smt2')
-rw-r--r-- | test/regress/regress1/sep/dispose-list-4-init.smt2 | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/test/regress/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2 new file mode 100644 index 000000000..b3e2088b1 --- /dev/null +++ b/test/regress/regress1/sep/dispose-list-4-init.smt2 @@ -0,0 +1,36 @@ +; 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) |