blob: 10ed4be7c7ad72ee41f782bd3899fc868cde9e01 (
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
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
(define-fun smt_set_emp () mySet (as emptyset mySet))
(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s))
(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x)))
(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
(declare-fun z3v66 () Int)
(declare-fun z3v67 () Int)
(assert (distinct z3v66 z3v67))
(declare-fun z3v68 () Int)
(declare-fun z3f69 (Int) Int)
(declare-fun z3f70 (Int) mySet)
(declare-fun z3v71 () Int)
(declare-fun z3f72 (Int) mySet)
(declare-fun z3v73 () Int)
(declare-fun z3v74 () Int)
(declare-fun z3v75 () Int)
(declare-fun z3f76 (Int) Bool)
(declare-fun z3f77 (Int Int) Int)
(declare-fun z3v78 () Int)
(declare-fun z3f79 (Int) Bool)
(declare-fun z3v80 () Int)
(declare-fun z3f81 (Int) Int)
(declare-fun z3v82 () Int)
(declare-fun z3v83 () Int)
(declare-fun z3v85 () Int)
(declare-fun z3v86 () Int)
(declare-fun z3v87 () Int)
(declare-fun z3f88 () Int)
(declare-fun z3v89 () Int)
(declare-fun z3v90 () Int)
(declare-fun z3v91 () Int)
(declare-fun z3v92 () Int)
(declare-fun z3v93 () Int)
(declare-fun z3f94 (Int) Int)
(declare-fun z3f95 (Int) Int)
(declare-fun z3f96 (Int Int Int) Int)
(declare-fun z3v97 () Int)
(declare-fun z3v98 () Int)
(declare-fun z3v99 () Int)
(assert (= z3v99 z3v98))
(assert (and (>= (z3f69 z3v85) 0)
(not (smt_set_mem z3v86 (z3f70 z3v85)))
(= (z3f72 z3v85) smt_set_emp)
(>= (z3f69 z3v87) 0)
(= (z3f72 z3v87) smt_set_emp)
(= (z3f70 z3v87) smt_set_emp)
(= (z3f69 z3v87) 0)
(= (z3f76 z3v87) true)
(= z3v87 z3f88)
(>= (z3f69 z3v87) 0)
(= z3v87 z3v89)
(>= (z3f69 z3v87) 0)
(= (z3f70 z3v87)
(z3f70 z3v90))
(= (z3f72 z3v87) smt_set_emp)
(>= (z3f69 z3v89) 0)
(= (z3f70 z3v89)
(z3f70 z3v90))
(= (z3f72 z3v89) smt_set_emp)
(>= (z3f69 z3v90) 0)
(= (z3f72 z3v90)
(ite (smt_set_mem z3v86 (z3f70 z3v85))
(smt_set_cup (smt_set_add smt_set_emp z3v86)
(z3f72 z3v85))
(z3f72 z3v85)))
(= (z3f70 z3v90)
(smt_set_cup (smt_set_add smt_set_emp z3v86)
(z3f70 z3v85)))
(= (z3f69 z3v90)
(+ 1 (z3f69 z3v85)))
(= (z3f76 z3v90) false)
(>= (z3f69 z3v91) 0)
(= (z3f72 z3v91) smt_set_emp)
(= (z3f70 z3v91) smt_set_emp)
(= (z3f69 z3v91) 0)
(= (z3f76 z3v91) true)
(= z3v91 z3f88)
(>= (z3f69 z3v91) 0)
(= z3v91 z3v92)
(>= (z3f69 z3v91) 0)
(not (smt_set_mem z3v86 (z3f70 z3v91)))
(= (z3f72 z3v91) smt_set_emp)
(= (z3f94 z3v93) z3v92)
(= (z3f95 z3v93) z3v85)
(= z3v93 (z3f96 z3v86 z3v92 z3v85))
(= z3v93 z3v97)
(= (smt_set_cap (z3f70 (z3f94 z3v93))
(z3f70 (z3f95 z3v93))) smt_set_emp)
(>= (z3f69 z3v92) 0)
(not (smt_set_mem z3v86 (z3f70 z3v92)))
(= (z3f72 z3v92) smt_set_emp)
(= (smt_set_cap (z3f70 (z3f94 z3v97))
(z3f70 (z3f95 z3v97))) smt_set_emp)
(z3f79 z3v66)
(= (z3f81 z3v80) z3v80)
(= (z3f81 z3v82) z3v82)
(not (z3f79 z3v67))
(= (z3f81 z3v83) z3v83)))
(assert (not (> z3v99 z3v98)))
(check-sat)
|
