author | wenzelm |
Sat, 05 Apr 2014 15:03:40 +0200 | |
changeset 56421 | 1ffd7eaa778b |
parent 56111 | 5b76e1790c38 |
child 56727 | 75f4fdafb285 |
permissions | -rw-r--r-- |
56111 | 1 |
d47653c43412ab1eb54730f2f5a4f4bdf44fcb5a 8 0 |
56109 | 2 |
unsat |
3 |
((set-logic <null>) |
|
4 |
(proof |
|
56111 | 5 |
(let ((@x36 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4)))))) |
6 |
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true)))) |
|
7 |
(let ((@x47 (trans (monotonicity @x40 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false)))) |
|
8 |
(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x47 false)))))) |
|
56109 | 9 |
|
56111 | 10 |
da258c2a22a4a00129b43deac09b90d379043340 7 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
11 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
12 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
13 |
(proof |
56111 | 14 |
(let ((@x33 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true))))) |
15 |
(let ((@x37 (trans @x33 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false)))) |
|
16 |
(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x37 false))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
17 |
|
56111 | 18 |
f2b47b92988d2f0c1404b109b621ba9a6c2b9d1c 7 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
19 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
20 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
21 |
(proof |
56111 | 22 |
(let ((@x36 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true))))) |
23 |
(let ((@x40 (trans @x36 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false)))) |
|
24 |
(mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x40 false))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
25 |
|
56111 | 26 |
1c22485fb98e3caa4d683df39ead427fc3568432 9 0 |
56109 | 27 |
unsat |
28 |
((set-logic <null>) |
|
29 |
(proof |
|
56111 | 30 |
(let ((@x36 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5)))))) |
31 |
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true)))) |
|
32 |
(let ((@x43 (monotonicity @x40 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true))))) |
|
33 |
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false)))) |
|
34 |
(mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x47 false))))))) |
|
56109 | 35 |
|
56111 | 36 |
651f74a079a4aa15d5d621208d8e038db0369475 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
37 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
38 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
39 |
(proof |
56111 | 40 |
(let ((@x36 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8)))))) |
41 |
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true)))) |
|
42 |
(let ((@x43 (monotonicity @x40 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true))))) |
|
43 |
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false)))) |
|
44 |
(mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x47 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
45 |
|
56111 | 46 |
eefb4f0a8b690f38fb11c31757b3209b40cfd1c5 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
47 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
48 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
49 |
(proof |
56111 | 50 |
(let ((@x41 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8)))))) |
51 |
(let ((@x45 (trans @x41 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true)))) |
|
52 |
(let ((@x48 (monotonicity @x45 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true))))) |
|
53 |
(let ((@x52 (trans @x48 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false)))) |
|
54 |
(mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x52 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
55 |
|
56111 | 56 |
e251dcc0ad168cb65c5bc1d32039c72ca2609bb3 7 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
57 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
58 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
59 |
(proof |
56111 | 60 |
(let ((@x33 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) |
61 |
(let ((@x37 (trans @x33 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) |
|
62 |
(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x37 false))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
63 |
|
56111 | 64 |
4f488dde65b4a70d1d31d589531d3445a9be689f 11 0 |
65 |
unsat |
|
66 |
((set-logic <null>) |
|
67 |
(proof |
|
68 |
(let ((@x40 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7)))))) |
|
69 |
(let ((@x45 (trans @x40 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7))))) |
|
70 |
(let ((@x50 (monotonicity @x45 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7)))))) |
|
71 |
(let ((@x54 (trans @x50 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true)))) |
|
72 |
(let ((@x57 (monotonicity @x54 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true))))) |
|
73 |
(let ((@x61 (trans @x57 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false)))) |
|
74 |
(mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x61 false))))))))) |
|
75 |
||
76 |
2e53bd8b513a3dc9dee350d0d8b1c315cf2b2449 19 0 |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
77 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
78 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
79 |
(proof |
56111 | 80 |
(let ((?x13 (bvadd |b$| |c$|))) |
81 |
(let ((?x14 (bvadd ?x13 |a$|))) |
|
82 |
(let ((?x8 (bvmul (_ bv2 32) |b$|))) |
|
83 |
(let ((?x9 (bvadd |a$| ?x8))) |
|
84 |
(let ((?x11 (bvadd ?x9 |c$|))) |
|
85 |
(let ((?x12 (bvsub ?x11 |b$|))) |
|
86 |
(let (($x15 (= ?x12 ?x14))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
87 |
(let (($x16 (not $x15))) |
56111 | 88 |
(let ((@x56 (rewrite (= (= (bvadd |a$| |b$| |c$|) (bvadd |a$| |b$| |c$|)) true)))) |
89 |
(let ((@x46 (rewrite (= (bvsub (bvadd |a$| ?x8 |c$|) |b$|) (bvadd |a$| |b$| |c$|))))) |
|
90 |
(let ((@x44 (monotonicity (rewrite (= ?x11 (bvadd |a$| ?x8 |c$|))) (= ?x12 (bvsub (bvadd |a$| ?x8 |c$|) |b$|))))) |
|
91 |
(let ((@x54 (monotonicity (trans @x44 @x46 (= ?x12 (bvadd |a$| |b$| |c$|))) (rewrite (= ?x14 (bvadd |a$| |b$| |c$|))) (= $x15 (= (bvadd |a$| |b$| |c$|) (bvadd |a$| |b$| |c$|)))))) |
|
92 |
(let ((@x61 (monotonicity (trans @x54 @x56 (= $x15 true)) (= $x16 (not true))))) |
|
93 |
(let ((@x65 (trans @x61 (rewrite (= (not true) false)) (= $x16 false)))) |
|
94 |
(mp (asserted $x16) @x65 false))))))))))))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
95 |
|
56111 | 96 |
570be43092e6421d4222501467362afbd680c2e2 18 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
97 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
98 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
99 |
(proof |
56111 | 100 |
(let ((?x9 (bvmul (_ bv4 4) |x$|))) |
101 |
(let (($x10 (= ?x9 (_ bv4 4)))) |
|
102 |
(let (($x41 (= (_ bv5 4) |x$|))) |
|
103 |
(let (($x54 (not (or (not $x41) (= (_ bv4 4) ?x9))))) |
|
104 |
(let ((@x46 (monotonicity (rewrite (= (= |x$| (_ bv5 4)) $x41)) (= (not (= |x$| (_ bv5 4))) (not $x41))))) |
|
105 |
(let ((@x53 (monotonicity @x46 (rewrite (= $x10 (= (_ bv4 4) ?x9))) (= (or (not (= |x$| (_ bv5 4))) $x10) (or (not $x41) (= (_ bv4 4) ?x9)))))) |
|
106 |
(let (($x12 (not (=> (= |x$| (_ bv5 4)) $x10)))) |
|
107 |
(let ((@x37 (rewrite (= (=> (= |x$| (_ bv5 4)) $x10) (or (not (= |x$| (_ bv5 4))) $x10))))) |
|
108 |
(let ((@x58 (trans (monotonicity @x37 (= $x12 (not (or (not (= |x$| (_ bv5 4))) $x10)))) (monotonicity @x53 (= (not (or (not (= |x$| (_ bv5 4))) $x10)) $x54)) (= $x12 $x54)))) |
|
109 |
(let ((@x65 (monotonicity (|not-or-elim| (mp (asserted $x12) @x58 $x54) $x41) (= ?x9 (bvmul (_ bv4 4) (_ bv5 4)))))) |
|
110 |
(let ((@x71 (monotonicity (trans @x65 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x10) (= (= (_ bv4 4) ?x9) (= (_ bv4 4) (_ bv4 4)))))) |
|
111 |
(let ((@x75 (trans @x71 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x9) true)))) |
|
112 |
(let ((@x82 (trans (monotonicity @x75 (= (not (= (_ bv4 4) ?x9)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x9)) false)))) |
|
113 |
(mp (|not-or-elim| (mp (asserted $x12) @x58 $x54) (not (= (_ bv4 4) ?x9))) @x82 false)))))))))))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
114 |
|
56111 | 115 |
2538d74409c652fbc39d33a15f25d18c9bb179bf 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
116 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
117 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
118 |
(proof |
56111 | 119 |
(let ((@x35 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32)))))) |
120 |
(let ((@x39 (trans @x35 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true)))) |
|
121 |
(let ((@x42 (monotonicity @x39 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true))))) |
|
122 |
(let ((@x46 (trans @x42 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false)))) |
|
123 |
(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x46 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
124 |
|
56111 | 125 |
ea3351a199ecbca8cfc913892024d6ba767f41dc 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
126 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
127 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
128 |
(proof |
56111 | 129 |
(let ((@x35 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8)))))) |
130 |
(let ((@x39 (trans @x35 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true)))) |
|
131 |
(let ((@x42 (monotonicity @x39 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true))))) |
|
132 |
(let ((@x46 (trans @x42 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false)))) |
|
133 |
(mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x46 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
134 |
|
56111 | 135 |
a36393e9d24b671ce68aafbd67bbc7bcd4c32a9f 9 0 |
136 |
unsat |
|
137 |
((set-logic <null>) |
|
138 |
(proof |
|
139 |
(let ((@x35 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8)))))) |
|
140 |
(let ((@x39 (trans @x35 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) |
|
141 |
(let ((@x42 (monotonicity @x39 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) |
|
142 |
(let ((@x46 (trans @x42 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) |
|
143 |
(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x46 false))))))) |
|
144 |
||
145 |
48dba82ab628843121b1cc45b6a662d4282a5dfd 8 0 |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
146 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
147 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
148 |
(proof |
56111 | 149 |
(let ((@x34 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) |
150 |
(let ((@x38 (trans @x34 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) |
|
151 |
(let ((@x45 (trans (monotonicity @x38 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false)))) |
|
152 |
(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x45 false)))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
153 |
|
56111 | 154 |
ffdba93b71ca27a7275f33b87244eb12ceb5e9c2 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
155 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
156 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
157 |
(proof |
56111 | 158 |
(let ((@x35 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) |
159 |
(let ((@x39 (trans @x35 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) |
|
160 |
(let ((@x42 (monotonicity @x39 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) |
|
161 |
(let ((@x46 (trans @x42 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) |
|
162 |
(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x46 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
163 |
|
56111 | 164 |
24677a2d05cd59ffe782bea3654e41f124fc1b93 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
165 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
166 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
167 |
(proof |
56111 | 168 |
(let ((@x35 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) |
169 |
(let ((@x39 (trans @x35 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) |
|
170 |
(let ((@x42 (monotonicity @x39 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) |
|
171 |
(let ((@x46 (trans @x42 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false)))) |
|
172 |
(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x46 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
173 |
|
56111 | 174 |
bf709bf2b13e6bf4f9668ad197c5d7a4ca581525 8 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
175 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
176 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
177 |
(proof |
56111 | 178 |
(let ((@x50 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2)))))) |
179 |
(let ((@x54 (trans @x50 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true)))) |
|
180 |
(let ((@x61 (trans (monotonicity @x54 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false)))) |
|
181 |
(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x61 false)))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
182 |
|
56111 | 183 |
f487669e8e249c60376443304a5a78c58eddd1cc 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
184 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
185 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
186 |
(proof |
56111 | 187 |
(let ((@x34 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10)))))) |
188 |
(let ((@x38 (trans @x34 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true)))) |
|
189 |
(let ((@x41 (monotonicity @x38 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true))))) |
|
190 |
(let ((@x45 (trans @x41 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false)))) |
|
191 |
(mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x45 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
192 |
|
56111 | 193 |
e6179d5000250fb81646a549216cd9ad7b2619a2 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
194 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
195 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
196 |
(proof |
56111 | 197 |
(let ((@x34 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6)))))) |
198 |
(let ((@x38 (trans @x34 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true)))) |
|
199 |
(let ((@x41 (monotonicity @x38 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true))))) |
|
200 |
(let ((@x45 (trans @x41 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false)))) |
|
201 |
(mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x45 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
202 |
|
56111 | 203 |
5ca573788c44ee26ee19907e7d9d9ec1635c9a5b 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
204 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
205 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
206 |
(proof |
56111 | 207 |
(let ((@x51 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8)))))) |
208 |
(let ((@x55 (trans @x51 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true)))) |
|
209 |
(let ((@x58 (monotonicity @x55 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true))))) |
|
210 |
(let ((@x62 (trans @x58 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false)))) |
|
211 |
(mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x62 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
212 |
|
56111 | 213 |
b4a2032ff1791888567d8f54fa94d95365cb3255 9 0 |
56109 | 214 |
unsat |
215 |
((set-logic <null>) |
|
216 |
(proof |
|
56111 | 217 |
(let ((@x51 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8)))))) |
218 |
(let ((@x55 (trans @x51 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true)))) |
|
219 |
(let ((@x58 (monotonicity @x55 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true))))) |
|
220 |
(let ((@x62 (trans @x58 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false)))) |
|
221 |
(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x62 false))))))) |
|
56109 | 222 |
|
56111 | 223 |
7a4f6966fce99a20413ba9068cef650098d5df66 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
224 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
225 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
226 |
(proof |
56111 | 227 |
(let ((@x51 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8)))))) |
228 |
(let ((@x55 (trans @x51 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true)))) |
|
229 |
(let ((@x58 (monotonicity @x55 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true))))) |
|
230 |
(let ((@x62 (trans @x58 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false)))) |
|
231 |
(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x62 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
232 |
|
56111 | 233 |
17e3ce1c7a7f4469b5b93e126887f9f5cc55a51d 9 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
234 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
235 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
236 |
(proof |
56111 | 237 |
(let ((@x50 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4)))))) |
238 |
(let ((@x54 (trans @x50 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true)))) |
|
239 |
(let ((@x57 (monotonicity @x54 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true))))) |
|
240 |
(let ((@x61 (trans @x57 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false)))) |
|
241 |
(mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x61 false))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
242 |
|
56111 | 243 |
070667ff72c73dc8cd9ebb50cc06803d9785fef4 9 0 |
244 |
unsat |
|
245 |
((set-logic <null>) |
|
246 |
(proof |
|
247 |
(let ((@x50 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4)))))) |
|
248 |
(let ((@x54 (trans @x50 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true)))) |
|
249 |
(let ((@x57 (monotonicity @x54 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true))))) |
|
250 |
(let ((@x61 (trans @x57 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false)))) |
|
251 |
(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x61 false))))))) |
|
252 |
||
253 |
222d5f4b74cc91bf83cca8b1b96f9cfe0f7db0f7 17 0 |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
254 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
255 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
256 |
(proof |
56109 | 257 |
(let ((?x9 (bvand |x$| (_ bv255 16)))) |
258 |
(let ((?x7 (bvand |x$| (_ bv65280 16)))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
259 |
(let ((?x10 (bvor ?x7 ?x9))) |
56109 | 260 |
(let (($x11 (= ?x10 |x$|))) |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
261 |
(let (($x12 (not $x11))) |
56111 | 262 |
(let ((@x57 (symm (commutativity (= (= |x$| ?x10) $x11)) (= $x11 (= |x$| ?x10))))) |
263 |
(let ((@x33 (asserted $x12))) |
|
264 |
(let ((@x61 (mp @x33 (monotonicity @x57 (= $x12 (not (= |x$| ?x10)))) (not (= |x$| ?x10))))) |
|
265 |
(let (($x50 (= |x$| ?x10))) |
|
266 |
(let ((@x32 (|true-axiom| true))) |
|
267 |
(let (($x51 (or $x50 false false false false false false false false false false false false false false false false))) |
|
268 |
(let ((@x53 (|unit-resolution| ((_ |th-lemma| bv) $x51) @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 $x50))) |
|
269 |
(|unit-resolution| @x53 @x61 false))))))))))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
270 |
|
56111 | 271 |
f856dea62e897c0065d5a1827265d3ff37ee50c8 51 0 |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
272 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
273 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
274 |
(proof |
56111 | 275 |
(let ((?x9 (bvand |w$| (_ bv255 16)))) |
276 |
(let (($x10 (= ?x9 |w$|))) |
|
277 |
(let (($x62 (not $x10))) |
|
278 |
(let ((@x316 (symm (commutativity (= (= |w$| ?x9) $x10)) (= $x10 (= |w$| ?x9))))) |
|
279 |
(let (($x55 (not (or (bvule (_ bv256 16) |w$|) $x10)))) |
|
280 |
(let ((@x47 (monotonicity (rewrite (= (bvult |w$| (_ bv256 16)) (not (bvule (_ bv256 16) |w$|)))) (= (not (bvult |w$| (_ bv256 16))) (not (not (bvule (_ bv256 16) |w$|))))))) |
|
281 |
(let ((@x51 (trans @x47 (rewrite (= (not (not (bvule (_ bv256 16) |w$|))) (bvule (_ bv256 16) |w$|))) (= (not (bvult |w$| (_ bv256 16))) (bvule (_ bv256 16) |w$|))))) |
|
282 |
(let ((@x54 (monotonicity @x51 (= (or (not (bvult |w$| (_ bv256 16))) $x10) (or (bvule (_ bv256 16) |w$|) $x10))))) |
|
283 |
(let ((@x57 (monotonicity @x54 (= (not (or (not (bvult |w$| (_ bv256 16))) $x10)) $x55)))) |
|
284 |
(let (($x12 (not (=> (bvult |w$| (_ bv256 16)) $x10)))) |
|
285 |
(let ((@x37 (rewrite (= (=> (bvult |w$| (_ bv256 16)) $x10) (or (not (bvult |w$| (_ bv256 16))) $x10))))) |
|
286 |
(let ((@x40 (monotonicity @x37 (= $x12 (not (or (not (bvult |w$| (_ bv256 16))) $x10)))))) |
|
287 |
(let ((@x63 (|not-or-elim| (mp (asserted $x12) (trans @x40 @x57 (= $x12 $x55)) $x55) $x62))) |
|
288 |
(let ((@x320 (mp @x63 (monotonicity @x316 (= $x62 (not (= |w$| ?x9)))) (not (= |w$| ?x9))))) |
|
289 |
(let (($x298 (= |w$| ?x9))) |
|
290 |
(let (($x79 (= ((_ extract 15 15) |w$|) (_ bv1 1)))) |
|
291 |
(let (($x262 (not $x79))) |
|
292 |
(let (($x72 (= ((_ extract 8 8) |w$|) (_ bv1 1)))) |
|
293 |
(let (($x73 (= ((_ extract 9 9) |w$|) (_ bv1 1)))) |
|
294 |
(let (($x80 (and $x73 $x72))) |
|
295 |
(let (($x81 (or $x73 $x72 $x80))) |
|
296 |
(let (($x74 (= ((_ extract 10 10) |w$|) (_ bv1 1)))) |
|
297 |
(let (($x82 (and $x74 $x81))) |
|
298 |
(let (($x83 (or $x74 $x73 $x72 $x80 $x82))) |
|
299 |
(let (($x75 (= ((_ extract 11 11) |w$|) (_ bv1 1)))) |
|
300 |
(let (($x84 (and $x75 $x83))) |
|
301 |
(let (($x85 (or $x75 $x74 $x73 $x72 $x80 $x82 $x84))) |
|
302 |
(let (($x76 (= ((_ extract 12 12) |w$|) (_ bv1 1)))) |
|
303 |
(let (($x86 (and $x76 $x85))) |
|
304 |
(let (($x87 (or $x76 $x75 $x74 $x73 $x72 $x80 $x82 $x84 $x86))) |
|
305 |
(let (($x77 (= ((_ extract 13 13) |w$|) (_ bv1 1)))) |
|
306 |
(let (($x88 (and $x77 $x87))) |
|
307 |
(let (($x89 (or $x77 $x76 $x75 $x74 $x73 $x72 $x80 $x82 $x84 $x86 $x88))) |
|
308 |
(let (($x78 (= ((_ extract 14 14) |w$|) (_ bv1 1)))) |
|
309 |
(let (($x90 (and $x78 $x89))) |
|
310 |
(let (($x91 (or $x78 $x77 $x76 $x75 $x74 $x73 $x72 $x80 $x82 $x84 $x86 $x88 $x90))) |
|
311 |
(let (($x92 (and $x79 $x91))) |
|
312 |
(let (($x93 (or $x79 $x78 $x77 $x76 $x75 $x74 $x73 $x72 $x80 $x82 $x84 $x86 $x88 $x90 $x92))) |
|
313 |
(let (($x295 (not $x93))) |
|
314 |
(let (($x41 (bvule (_ bv256 16) |w$|))) |
|
315 |
(let (($x42 (not $x41))) |
|
316 |
(let ((@x61 (|not-or-elim| (mp (asserted $x12) (trans @x40 @x57 (= $x12 $x55)) $x55) $x42))) |
|
317 |
(let ((@x301 (|unit-resolution| ((_ |th-lemma| bv) (or $x41 $x295)) @x61 $x295))) |
|
318 |
(let ((@x32 (|true-axiom| true))) |
|
319 |
(let (($x310 (or $x298 false false false false false false false false $x72 $x73 $x74 $x75 $x76 $x77 $x78 $x79))) |
|
320 |
(let ((@x312 (|unit-resolution| ((_ |th-lemma| bv) $x310) @x32 @x32 @x32 @x32 @x32 @x32 @x32 @x32 (|unit-resolution| (|def-axiom| (or $x93 (not $x72))) @x301 (not $x72)) (|unit-resolution| (|def-axiom| (or $x93 (not $x73))) @x301 (not $x73)) (|unit-resolution| (|def-axiom| (or $x93 (not $x74))) @x301 (not $x74)) (|unit-resolution| (|def-axiom| (or $x93 (not $x75))) @x301 (not $x75)) (|unit-resolution| (|def-axiom| (or $x93 (not $x76))) @x301 (not $x76)) (|unit-resolution| (|def-axiom| (or $x93 (not $x77))) @x301 (not $x77)) (|unit-resolution| (|def-axiom| (or $x93 (not $x78))) @x301 (not $x78)) (|unit-resolution| (|def-axiom| (or $x93 $x262)) @x301 $x262) $x298))) |
|
321 |
(|unit-resolution| @x312 @x320 false))))))))))))))))))))))))))))))))))))))))))))))))) |
|
322 |
||
323 |
39d6b3ac211187a764a365cb2d10eb3330116060 29 0 |
|
324 |
unsat |
|
325 |
((set-logic <null>) |
|
326 |
(proof |
|
327 |
(let ((?x6 (|bv2int$| (_ bv0 2)))) |
|
328 |
(let (($x181 (<= ?x6 0))) |
|
329 |
(let (($x182 (not $x181))) |
|
330 |
(let (($x173 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x22 (|bv2int$| ?v0))) |
|
331 |
(let (($x59 (<= ?x22 0))) |
|
332 |
(not $x59))) :pattern ( (|bv2int$| ?v0) ))) |
|
56109 | 333 |
)) |
56111 | 334 |
(let (($x63 (forall ((?v0 (_ BitVec 2)) )(let ((?x22 (|bv2int$| ?v0))) |
335 |
(let (($x59 (<= ?x22 0))) |
|
336 |
(not $x59)))) |
|
56109 | 337 |
)) |
56111 | 338 |
(let ((@x175 (refl (= (not (<= (|bv2int$| ?0) 0)) (not (<= (|bv2int$| ?0) 0)))))) |
339 |
(let ((@x110 (refl (|~| (not (<= (|bv2int$| ?0) 0)) (not (<= (|bv2int$| ?0) 0)))))) |
|
56109 | 340 |
(let (($x24 (forall ((?v0 (_ BitVec 2)) )(let ((?x22 (|bv2int$| ?v0))) |
341 |
(< 0 ?x22))) |
|
342 |
)) |
|
56111 | 343 |
(let ((@x62 (rewrite (= (< 0 (|bv2int$| ?0)) (not (<= (|bv2int$| ?0) 0)))))) |
344 |
(let ((@x113 (|mp~| (mp (asserted $x24) (|quant-intro| @x62 (= $x24 $x63)) $x63) (|nnf-pos| @x110 (|~| $x63 $x63)) $x63))) |
|
345 |
(let ((@x178 (mp @x113 (|quant-intro| @x175 (= $x63 $x173)) $x173))) |
|
346 |
(let (($x185 (not $x173))) |
|
347 |
(let (($x186 (or $x185 $x182))) |
|
348 |
(let ((@x187 ((_ |quant-inst| (_ bv0 2)) $x186))) |
|
349 |
(let (($x8 (= ?x6 0))) |
|
350 |
(let ((@x52 (asserted $x8))) |
|
351 |
(|unit-resolution| ((_ |th-lemma| arith triangle-eq) (or (not $x8) $x181)) @x52 (|unit-resolution| @x187 @x178 $x182) false))))))))))))))))))) |
|
56109 | 352 |
|
56111 | 353 |
f7db43c56c17d090679f2e9727e9eaa7cf84ab8d 16 0 |
56109 | 354 |
unsat |
355 |
((set-logic <null>) |
|
356 |
(proof |
|
357 |
(let ((?x10 (|p$| true))) |
|
56111 | 358 |
(let (($x7 (bvule (_ bv0 4) |a$|))) |
359 |
(let (($x8 (ite $x7 true false))) |
|
360 |
(let ((?x9 (|p$| $x8))) |
|
361 |
(let (($x11 (= ?x9 ?x10))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
362 |
(let (($x12 (not $x11))) |
56111 | 363 |
(let ((@x50 (monotonicity (monotonicity (rewrite (= $x7 true)) (= (|p$| $x7) ?x10)) (= (= (|p$| $x7) ?x10) (= ?x10 ?x10))))) |
364 |
(let ((@x54 (trans @x50 (rewrite (= (= ?x10 ?x10) true)) (= (= (|p$| $x7) ?x10) true)))) |
|
365 |
(let ((@x61 (trans (monotonicity @x54 (= (not (= (|p$| $x7) ?x10)) (not true))) (rewrite (= (not true) false)) (= (not (= (|p$| $x7) ?x10)) false)))) |
|
366 |
(let ((@x41 (monotonicity (monotonicity (rewrite (= $x8 $x7)) (= ?x9 (|p$| $x7))) (= $x11 (= (|p$| $x7) ?x10))))) |
|
367 |
(let ((@x44 (monotonicity @x41 (= $x12 (not (= (|p$| $x7) ?x10)))))) |
|
368 |
(mp (asserted $x12) (trans @x44 @x61 (= $x12 false)) false)))))))))))))) |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
369 |