/
ls_odd_split_ls_even_odd.sb.smt2
77 lines (61 loc) · 1.18 KB
/
ls_odd_split_ls_even_odd.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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
(set-logic SHID)
(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)))))
(declare-heap (Refnode node))
;; heap predicates
(define-funs-rec (
(ls ((x_1 Refnode) (y_2 Refnode)) Bool)
(leven ((x_4 Refnode) (y_5 Refnode)) Bool)
(lodd ((x_7 Refnode) (y_8 Refnode)) Bool)
)
(
(or
(and
(_ emp Refnode node)
(= x_1 y_2))
(exists
((u_3 Refnode))
(sep
(pto x_1 (c_node u_3))
(ls u_3 y_2))))
;; heap predicates
(or
(and
(_ emp Refnode node)
(= x_4 y_5))
(exists
((u_6 Refnode))
(sep
(pto x_4 (c_node u_6))
(lodd u_6 y_5))))
;; heap predicates
(or
(pto x_7 (c_node y_8))
(exists
((u_9 Refnode))
(sep
(pto x_7 (c_node u_9))
(leven u_9 y_8))))
)
)
(check-sat)
;; entailment: lodd(x,y) |- (exists t. leven(t,y) * lodd(x,t))
(declare-const x Refnode)
(declare-const y Refnode)
(assert
(lodd x y))
(assert
(not
(exists
((t Refnode))
(sep
(leven t y)
(lodd x t)))))
(check-sat)