/
dll_ubnd_len_get_5_lasts.sb.smt2
63 lines (51 loc) · 1.37 KB
/
dll_ubnd_len_get_5_lasts.sb.smt2
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(set-logic SHIDLIA)
(set-info :source | Songbird - https://songbird-prover.github.io/ |)
(set-info :smt-lib-version 2)
(set-info :category "crafted")
(set-info :status unsat)
;; singleton heap
(declare-sort Refnode 0)
(declare-datatypes
((node 0))
(((c_node (next Refnode) (prev Refnode)))))
(declare-heap (Refnode node))
;; heap predicates
(define-fun-rec dll ((hd_1 Refnode) (p_2 Refnode) (tl_3 Refnode) (n_4 Refnode) (len_5 Int)) Bool
(or
(and
(pto hd_1 (c_node n_4 p_2))
(and
(= (- len_5 1) 0)
(= hd_1 tl_3)))
(exists
((x_6 Refnode) (k Int))
(and
(sep
(pto hd_1 (c_node x_6 p_2))
(dll x_6 hd_1 tl_3 n_4 k))
(= k (- len_5 1))
(<= 1 (- len_5 1))))))
(check-sat)
;; entailment: dll(x,y,z,t,n) & 1000<=n |- (exists u1,u2,u3,u4,u5. u2->node{u3,u1} * u3->node{u4,u2} * u4->node{u5,u3} * u5->node{z,u4} * z->node{t,u5} * dll(x,y,u1,u2,n-5))
(declare-const x Refnode)
(declare-const y Refnode)
(declare-const z Refnode)
(declare-const t Refnode)
(declare-const n Int)
(assert
(and
(dll x y z t n)
(<= 1000 n)))
(assert
(not
(exists
((u1 Refnode) (u2 Refnode) (u3 Refnode) (u4 Refnode) (u5 Refnode) (k Int))
(and
(sep
(pto u2 (c_node u3 u1))
(pto u3 (c_node u4 u2))
(pto u4 (c_node u5 u3))
(pto u5 (c_node z u4))
(pto z (c_node t u5))
(dll x y u1 u2 k)) (= k (+ n (- 5)))))))
(check-sat)