blob: e9915bf4b7ad391b4469e115891070188c48a085 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_ALL)
(declare-sort Loc 0)
(declare-heap (Loc Loc))
(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)
|
