author | blanchet |
Thu, 13 Mar 2014 13:18:13 +0100 | |
changeset 56079 | 175ac95720d4 |
child 56109 | 1ba56358eba4 |
permissions | -rw-r--r-- |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
1 |
a438ed86857e9b990f36b8fba1876d2ee3208e44 8 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
2 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
3 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
4 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
5 |
(let ((@x17 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
6 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
7 |
(let ((@x28 (trans (monotonicity @x21 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
8 |
(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x28 false)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
9 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
10 |
9b71beed4cadbb1c6e2962eb013e86c8f71abf17 9 0 |
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 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
14 |
(let ((@x20 (monotonicity (rewrite (= (bvule (_ bv27 8) (_ bv23 8)) false)) (= (not (bvule (_ bv27 8) (_ bv23 8))) (not false))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
15 |
(let ((@x24 (trans @x20 (rewrite (= (not false) true)) (= (not (bvule (_ bv27 8) (_ bv23 8))) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
16 |
(let ((@x26 (trans (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) (not (bvule (_ bv27 8) (_ bv23 8))))) @x24 (= (bvult (_ bv23 8) (_ bv27 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
17 |
(let ((@x33 (trans (monotonicity @x26 (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true))) (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
18 |
(mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x33 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
19 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
20 |
83e5e97d82127f63e5519904051508641143369d 7 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
21 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
22 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
23 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
24 |
(let ((@x15 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
25 |
(let ((@x19 (trans @x15 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
26 |
(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x19 false))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
27 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
28 |
1e5c1dd05129223256f56ebbd2d47effcee4561c 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
29 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
30 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
31 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
32 |
(let ((@x17 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
33 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
34 |
(let ((@x24 (monotonicity @x21 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
35 |
(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
36 |
(mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x28 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
37 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
38 |
2999cde57fdda8b4770e92440b939692e4a6aa5f 12 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
39 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
40 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
41 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
42 |
(let ((@x25 (monotonicity (rewrite (= (bvmul (_ bv255 8) (_ bv27 8)) (_ bv229 8))) (= (bvadd (_ bv11 8) (bvmul (_ bv255 8) (_ bv27 8))) (bvadd (_ bv11 8) (_ bv229 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
43 |
(let ((@x30 (trans @x25 (rewrite (= (bvadd (_ bv11 8) (_ bv229 8)) (_ bv240 8))) (= (bvadd (_ bv11 8) (bvmul (_ bv255 8) (_ bv27 8))) (_ bv240 8))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
44 |
(let ((@x32 (trans (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (bvadd (_ bv11 8) (bvmul (_ bv255 8) (_ bv27 8))))) @x30 (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
45 |
(let ((@x37 (monotonicity @x32 (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
46 |
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
47 |
(let ((@x44 (monotonicity @x41 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
48 |
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
49 |
(mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x48 false)))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
50 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
51 |
5276e53d12319b7263028b7b35a0e825901a044d 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
52 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
53 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
54 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
55 |
(let ((@x17 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
56 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
57 |
(let ((@x24 (monotonicity @x21 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
58 |
(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
59 |
(mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x28 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
60 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
61 |
234b2b4e895fc2df774f19f02134d0ca4a5a16a1 7 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
62 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
63 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
64 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
65 |
(let ((@x15 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
66 |
(let ((@x19 (trans @x15 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
67 |
(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x19 false))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
68 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
69 |
dc503704730fb3b59f839ff9f108d372052a8660 11 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
70 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
71 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
72 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
73 |
(let ((@x21 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
74 |
(let ((@x26 (trans @x21 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
75 |
(let ((@x31 (monotonicity @x26 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
76 |
(let ((@x35 (trans @x31 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
77 |
(let ((@x38 (monotonicity @x35 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
78 |
(let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
79 |
(mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x42 false))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
80 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
81 |
a1e71f94523b4cd464028b84ee475aaff660cb0f 16 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
82 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
83 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
84 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
85 |
(let ((?x12 (bvsub (bvadd (bvadd |$a| (bvmul (_ bv2 32) |$b|)) |$c|) |$b|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
86 |
(let (($x15 (= ?x12 (bvadd (bvadd |$b| |$c|) |$a|)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
87 |
(let (($x16 (not $x15))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
88 |
(let ((@x45 (rewrite (= (= (bvadd |$a| |$b| |$c|) (bvadd |$b| |$c| |$a|)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
89 |
(let ((?x33 (bvadd |$a| |$b| |$c|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
90 |
(let ((?x20 (bvadd |$a| (bvmul (_ bv2 32) |$b|) |$c|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
91 |
(let ((?x28 (bvadd ?x20 (bvmul (_ bv4294967295 32) |$b|)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
92 |
(let ((@x25 (monotonicity (rewrite (= (bvadd (bvadd |$a| (bvmul (_ bv2 32) |$b|)) |$c|) ?x20)) (= ?x12 (bvsub ?x20 |$b|))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
93 |
(let ((@x37 (trans (trans @x25 (rewrite (= (bvsub ?x20 |$b|) ?x28)) (= ?x12 ?x28)) (rewrite (= ?x28 ?x33)) (= ?x12 ?x33)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
94 |
(let ((@x43 (monotonicity @x37 (rewrite (= (bvadd (bvadd |$b| |$c|) |$a|) (bvadd |$b| |$c| |$a|))) (= $x15 (= ?x33 (bvadd |$b| |$c| |$a|)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
95 |
(let ((@x50 (monotonicity (trans @x43 @x45 (= $x15 true)) (= $x16 (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
96 |
(mp (asserted $x16) (trans @x50 (rewrite (= (not true) false)) (= $x16 false)) false)))))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
97 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
98 |
07ce4ddeaf1a897fd86c82ea0be2917368402c4b 14 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
99 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
100 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
101 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
102 |
(let (($x10 (= (bvmul (_ bv4 4) |$x|) (_ bv4 4)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
103 |
(let (($x7 (= |$x| (_ bv5 4)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
104 |
(let ((@x22 (monotonicity (rewrite (= (=> $x7 $x10) (or (not $x7) $x10))) (= (not (=> $x7 $x10)) (not (or (not $x7) $x10)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
105 |
(let ((@x24 (|not-or-elim| (mp (asserted (not (=> $x7 $x10))) @x22 (not (or (not $x7) $x10))) $x7))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
106 |
(let ((@x32 (trans (monotonicity @x24 (= (bvmul (_ bv4 4) |$x|) (bvmul (_ bv4 4) (_ bv5 4)))) (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x10))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
107 |
(let ((@x39 (trans (monotonicity @x32 (= $x10 (= (_ bv4 4) (_ bv4 4)))) (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= $x10 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
108 |
(let ((@x46 (trans (monotonicity @x39 (= (not $x10) (not true))) (rewrite (= (not true) false)) (= (not $x10) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
109 |
(let (($x25 (not $x10))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
110 |
(let ((@x26 (|not-or-elim| (mp (asserted (not (=> $x7 $x10))) @x22 (not (or (not $x7) $x10))) $x25))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
111 |
(mp @x26 @x46 false)))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
112 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
113 |
bf082d012c77348e9e5c8d77f54b71808a9a2b45 13 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
114 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
115 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
116 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
117 |
(let (($x9 (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
118 |
(let ((@x28 (monotonicity (rewrite (= (bvnot (_ bv6 32)) (_ bv4294967289 32))) (rewrite (= (bvnot (_ bv5 32)) (_ bv4294967290 32))) (= (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32))) (bvor (_ bv4294967289 32) (_ bv4294967290 32)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
119 |
(let ((@x33 (trans @x28 (rewrite (= (bvor (_ bv4294967289 32) (_ bv4294967290 32)) (_ bv4294967291 32))) (= (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32))) (_ bv4294967291 32))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
120 |
(let ((@x36 (monotonicity @x33 (= (bvnot (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32)))) (bvnot (_ bv4294967291 32)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
121 |
(let ((@x40 (trans @x36 (rewrite (= (bvnot (_ bv4294967291 32)) (_ bv4 32))) (= (bvnot (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32)))) (_ bv4 32))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
122 |
(let ((@x19 (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (bvnot (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32)))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
123 |
(let ((@x48 (trans (monotonicity (trans @x19 @x40 $x9) (= $x9 (= (_ bv4 32) (_ bv4 32)))) (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= $x9 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
124 |
(let ((@x55 (trans (monotonicity @x48 (= (not $x9) (not true))) (rewrite (= (not true) false)) (= (not $x9) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
125 |
(mp (asserted (not $x9)) @x55 false))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
126 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
127 |
224e3adf486b015b2b86fd13b422d3432d5dd2ea 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
128 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
129 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
130 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
131 |
(let ((@x17 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
132 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
133 |
(let ((@x24 (monotonicity @x21 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
134 |
(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
135 |
(mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x28 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
136 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
137 |
6f410cdf4d96b9ee8b7b886db44e51fe495aad40 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
138 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
139 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
140 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
141 |
(let ((@x17 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
142 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
143 |
(let ((@x24 (monotonicity @x21 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
144 |
(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
145 |
(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x28 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
146 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
147 |
75e911429d9da77b77c961a3f11bf4fae39c1289 8 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
148 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
149 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
150 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
151 |
(let ((@x16 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
152 |
(let ((@x20 (trans @x16 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
153 |
(let ((@x27 (trans (monotonicity @x20 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
154 |
(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x27 false)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
155 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
156 |
144996e0132e6e5e8657189d4b8fc16447f15f7f 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
157 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
158 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
159 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
160 |
(let ((@x17 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
161 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
162 |
(let ((@x24 (monotonicity @x21 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
163 |
(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
164 |
(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x28 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
165 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
166 |
dedf960210e12ce3dfe685dabb09a7ae103a6b34 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
167 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
168 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
169 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
170 |
(let ((@x17 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
171 |
(let ((@x21 (trans @x17 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
172 |
(let ((@x24 (monotonicity @x21 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
173 |
(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
174 |
(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x28 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
175 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
176 |
efa324caae835caf47cbb2d21e18358840d28baa 8 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
177 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
178 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
179 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
180 |
(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
181 |
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
182 |
(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
183 |
(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
184 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
185 |
21eb47482df6fb5cf3198774bf96beedaec719a7 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
186 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
187 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
188 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
189 |
(let (($x8 (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
190 |
(let ((@x19 (trans (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (concat (_ bv0 6) (_ bv10 4)))) (rewrite (= (concat (_ bv0 6) (_ bv10 4)) (_ bv10 10))) $x8))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
191 |
(let ((@x26 (trans (monotonicity @x19 (= $x8 (= (_ bv10 10) (_ bv10 10)))) (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= $x8 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
192 |
(let ((@x33 (trans (monotonicity @x26 (= (not $x8) (not true))) (rewrite (= (not true) false)) (= (not $x8) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
193 |
(mp (asserted (not $x8)) @x33 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
194 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
195 |
4b811cc374f3df84ff1252430c602976203f62f2 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
196 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
197 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
198 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
199 |
(let ((@x16 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
200 |
(let ((@x20 (trans @x16 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
201 |
(let ((@x23 (monotonicity @x20 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
202 |
(let ((@x27 (trans @x23 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
203 |
(mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x27 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
204 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
205 |
80eccdbf8bbcc6ea1d4f3857bd01f3a1ad159ef2 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
206 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
207 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
208 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
209 |
(let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
210 |
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
211 |
(let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
212 |
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
213 |
(mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
214 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
215 |
97eb054e915337f30396aae674e0c82d561ec48b 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
216 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
217 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
218 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
219 |
(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
220 |
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
221 |
(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
222 |
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
223 |
(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
224 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
225 |
a91b3649f65952bf743777b618e6da6b37fcc95f 9 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
226 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
227 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
228 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
229 |
(let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
230 |
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
231 |
(let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
232 |
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
233 |
(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
234 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
235 |
329e4f3ee0408af9d367ae6246fb53276a50a32f 11 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
236 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
237 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
238 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
239 |
(let (($x8 (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
240 |
(let ((@x45 (monotonicity (rewrite (= ((_ extract 2 0) (_ bv14 4)) (_ bv6 3))) (rewrite (= ((_ extract 3 3) (_ bv14 4)) (_ bv1 1))) (= (concat ((_ extract 2 0) (_ bv14 4)) ((_ extract 3 3) (_ bv14 4))) (concat (_ bv6 3) (_ bv1 1)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
241 |
(let ((@x49 (trans @x45 (rewrite (= (concat (_ bv6 3) (_ bv1 1)) (_ bv13 4))) (= (concat ((_ extract 2 0) (_ bv14 4)) ((_ extract 3 3) (_ bv14 4))) (_ bv13 4))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
242 |
(let ((@x50 (trans (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (concat ((_ extract 2 0) (_ bv14 4)) ((_ extract 3 3) (_ bv14 4))))) @x49 $x8))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
243 |
(let ((@x57 (trans (monotonicity @x50 (= $x8 (= (_ bv13 4) (_ bv13 4)))) (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= $x8 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
244 |
(let ((@x64 (trans (monotonicity @x57 (= (not $x8) (not true))) (rewrite (= (not true) false)) (= (not $x8) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
245 |
(mp (asserted (not $x8)) @x64 false))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
246 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
247 |
591572ec6e8cad807a5a51108eafba79636afecf 11 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
248 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
249 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
250 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
251 |
(let (($x8 (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
252 |
(let ((@x46 (monotonicity (rewrite (= ((_ extract 1 0) (_ bv6 4)) (_ bv2 2))) (rewrite (= ((_ extract 3 2) (_ bv6 4)) (_ bv1 2))) (= (concat ((_ extract 1 0) (_ bv6 4)) ((_ extract 3 2) (_ bv6 4))) (concat (_ bv2 2) (_ bv1 2)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
253 |
(let ((@x50 (trans @x46 (rewrite (= (concat (_ bv2 2) (_ bv1 2)) (_ bv9 4))) (= (concat ((_ extract 1 0) (_ bv6 4)) ((_ extract 3 2) (_ bv6 4))) (_ bv9 4))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
254 |
(let ((@x37 (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (concat ((_ extract 1 0) (_ bv6 4)) ((_ extract 3 2) (_ bv6 4))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
255 |
(let ((@x58 (trans (monotonicity (trans @x37 @x50 $x8) (= $x8 (= (_ bv9 4) (_ bv9 4)))) (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= $x8 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
256 |
(let ((@x65 (trans (monotonicity @x58 (= (not $x8) (not true))) (rewrite (= (not true) false)) (= (not $x8) false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
257 |
(mp (asserted (not $x8)) @x65 false))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
258 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
259 |
06e703e92f9238355e516e861c984a3eb7d984a8 44 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
260 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
261 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
262 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
263 |
(let ((?x9 (bvand |$x| (_ bv255 16)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
264 |
(let ((?x7 (bvand |$x| (_ bv65280 16)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
265 |
(let ((?x10 (bvor ?x7 ?x9))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
266 |
(let (($x11 (= ?x10 |$x|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
267 |
(let (($x12 (not $x11))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
268 |
(let ((?x113 (concat ((_ extract 15 8) (concat ((_ extract 15 8) |$x|) (_ bv0 8))) ((_ extract 7 0) (concat (_ bv0 8) ((_ extract 7 0) |$x|)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
269 |
(let ((@x124 (monotonicity (rewrite (= ((_ extract 15 8) (concat ((_ extract 15 8) |$x|) (_ bv0 8))) ((_ extract 15 8) |$x|))) (rewrite (= ((_ extract 7 0) (concat (_ bv0 8) ((_ extract 7 0) |$x|))) ((_ extract 7 0) |$x|))) (= ?x113 (concat ((_ extract 15 8) |$x|) ((_ extract 7 0) |$x|)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
270 |
(let ((@x129 (trans @x124 (rewrite (= (concat ((_ extract 15 8) |$x|) ((_ extract 7 0) |$x|)) ((_ extract 15 0) |$x|))) (= ?x113 ((_ extract 15 0) |$x|))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
271 |
(let (($x114 (= (bvor (concat ((_ extract 15 8) |$x|) (_ bv0 8)) (concat (_ bv0 8) ((_ extract 7 0) |$x|))) ?x113))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
272 |
(let (($x109 (= ?x10 (bvor (concat ((_ extract 15 8) |$x|) (_ bv0 8)) (concat (_ bv0 8) ((_ extract 7 0) |$x|)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
273 |
(let ((?x81 ((_ extract 7 0) |$x|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
274 |
(let ((?x101 (concat (_ bv0 8) ?x81))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
275 |
(let ((?x16 (bvnot |$x|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
276 |
(let ((?x66 (bvor ?x16 (bvnot (_ bv255 16))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
277 |
(let ((?x67 (bvnot ?x66))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
278 |
(let ((@x103 (monotonicity (rewrite (= (bvnot (_ bv255 8)) (_ bv0 8))) (rewrite (= (bvnot (bvnot ?x81)) ?x81)) (= (concat (bvnot (_ bv255 8)) (bvnot (bvnot ?x81))) ?x101)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
279 |
(let ((?x47 (bvnot (_ bv255 8)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
280 |
(let ((?x94 (concat ?x47 (bvnot (bvnot ?x81))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
281 |
(let ((@x87 (monotonicity (rewrite (= ((_ extract 7 0) ?x16) (bvnot ?x81))) (= (concat (_ bv255 8) ((_ extract 7 0) ?x16)) (concat (_ bv255 8) (bvnot ?x81)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
282 |
(let ((@x74 (monotonicity (rewrite (= (bvnot (_ bv255 16)) (_ bv65280 16))) (= ?x66 (bvor ?x16 (_ bv65280 16)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
283 |
(let ((@x80 (trans @x74 (rewrite (= (bvor ?x16 (_ bv65280 16)) (concat (_ bv255 8) ((_ extract 7 0) ?x16)))) (= ?x66 (concat (_ bv255 8) ((_ extract 7 0) ?x16)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
284 |
(let ((@x92 (monotonicity (trans @x80 @x87 (= ?x66 (concat (_ bv255 8) (bvnot ?x81)))) (= ?x67 (bvnot (concat (_ bv255 8) (bvnot ?x81))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
285 |
(let ((@x98 (trans @x92 (rewrite (= (bvnot (concat (_ bv255 8) (bvnot ?x81))) ?x94)) (= ?x67 ?x94)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
286 |
(let ((@x107 (trans (rewrite (= ?x9 ?x67)) (trans @x98 @x103 (= ?x67 ?x101)) (= ?x9 ?x101)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
287 |
(let ((?x34 ((_ extract 15 8) |$x|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
288 |
(let ((?x58 (concat ?x34 (_ bv0 8)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
289 |
(let ((?x48 (concat (bvnot (bvnot ?x34)) ?x47))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
290 |
(let ((@x60 (monotonicity (rewrite (= (bvnot (bvnot ?x34)) ?x34)) (rewrite (= ?x47 (_ bv0 8))) (= ?x48 ?x58)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
291 |
(let ((?x18 (bvor ?x16 (bvnot (_ bv65280 16))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
292 |
(let ((?x19 (bvnot ?x18))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
293 |
(let ((@x40 (monotonicity (rewrite (= ((_ extract 15 8) ?x16) (bvnot ?x34))) (= (concat ((_ extract 15 8) ?x16) (_ bv255 8)) (concat (bvnot ?x34) (_ bv255 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
294 |
(let ((@x26 (monotonicity (rewrite (= (bvnot (_ bv65280 16)) (_ bv255 16))) (= ?x18 (bvor ?x16 (_ bv255 16)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
295 |
(let ((@x33 (trans @x26 (rewrite (= (bvor ?x16 (_ bv255 16)) (concat ((_ extract 15 8) ?x16) (_ bv255 8)))) (= ?x18 (concat ((_ extract 15 8) ?x16) (_ bv255 8)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
296 |
(let ((@x45 (monotonicity (trans @x33 @x40 (= ?x18 (concat (bvnot ?x34) (_ bv255 8)))) (= ?x19 (bvnot (concat (bvnot ?x34) (_ bv255 8))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
297 |
(let ((@x52 (trans @x45 (rewrite (= (bvnot (concat (bvnot ?x34) (_ bv255 8))) ?x48)) (= ?x19 ?x48)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
298 |
(let ((@x64 (trans (rewrite (= ?x7 ?x19)) (trans @x52 @x60 (= ?x19 ?x58)) (= ?x7 ?x58)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
299 |
(let ((@x134 (trans (trans (monotonicity @x64 @x107 $x109) (rewrite $x114) (= ?x10 ?x113)) (trans @x129 (rewrite (= ((_ extract 15 0) |$x|) |$x|)) (= ?x113 |$x|)) $x11))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
300 |
(let ((@x141 (trans (monotonicity @x134 (= $x11 (= |$x| |$x|))) (rewrite (= (= |$x| |$x|) true)) (= $x11 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
301 |
(let ((@x148 (trans (monotonicity @x141 (= $x12 (not true))) (rewrite (= (not true) false)) (= $x12 false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
302 |
(mp (asserted $x12) @x148 false)))))))))))))))))))))))))))))))))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
303 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
304 |
9e9d8bb4c49a1669973a1c2e9f8c033d853f6801 97 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
305 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
306 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
307 |
(declare-fun k!150 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
308 |
(declare-fun k!140 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
309 |
(declare-fun k!130 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
310 |
(declare-fun k!120 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
311 |
(declare-fun k!110 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
312 |
(declare-fun k!100 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
313 |
(declare-fun k!90 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
314 |
(declare-fun k!80 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
315 |
(declare-fun k!70 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
316 |
(declare-fun k!60 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
317 |
(declare-fun k!50 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
318 |
(declare-fun k!40 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
319 |
(declare-fun k!30 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
320 |
(declare-fun k!20 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
321 |
(declare-fun k!10 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
322 |
(declare-fun k!00 () Bool) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
323 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
324 |
(let (($x199 (or k!80 k!90 k!100 k!110 k!120 k!130 k!140 k!150))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
325 |
(let (($x364 (= (or false false false false false false false false) false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
326 |
(let (($x362 (= $x199 (or false false false false false false false false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
327 |
(let (($x312 (= k!150 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
328 |
(let ((@x316 (symm (rewrite (= $x312 (not k!150))) (= (not k!150) $x312)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
329 |
(let (($x143 (not k!150))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
330 |
(let (($x119 (not (or k!90 k!80 (not (or (not k!90) (not k!80))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
331 |
(let (($x118 (not k!100))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
332 |
(let (($x122 (or k!100 (or k!90 k!80 (not (or (not k!90) (not k!80)))) (not (or $x118 $x119))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
333 |
(let (($x123 (not k!110))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
334 |
(let (($x128 (not k!120))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
335 |
(let (($x131 (not (or $x128 (not (or k!110 $x122 (not (or $x123 (not $x122))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
336 |
(let (($x134 (not (or k!120 (or k!110 $x122 (not (or $x123 (not $x122)))) $x131)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
337 |
(let (($x133 (not k!130))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
338 |
(let (($x137 (or k!130 (or k!120 (or k!110 $x122 (not (or $x123 (not $x122)))) $x131) (not (or $x133 $x134))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
339 |
(let (($x138 (not k!140))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
340 |
(let (($x146 (not (or $x143 (not (or k!140 $x137 (not (or $x138 (not $x137))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
341 |
(let (($x147 (or k!150 (or k!140 $x137 (not (or $x138 (not $x137)))) $x146))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
342 |
(let ((?x107 (mkbv k!00 k!10 k!20 k!30 k!40 k!50 k!60 k!70 k!80 k!90 k!100 k!110 k!120 k!130 k!140 k!150))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
343 |
(let ((?x88 (mkbv false false false false false false false false true false false false false false false false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
344 |
(let ((@x109 (rewrite (= |$w| ?x107)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
345 |
(let ((@x112 (monotonicity (rewrite (= (_ bv256 16) ?x88)) @x109 (= (bvule (_ bv256 16) |$w|) (bvule ?x88 ?x107))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
346 |
(let ((@x151 (trans @x112 (rewrite (= (bvule ?x88 ?x107) $x147)) (= (bvule (_ bv256 16) |$w|) $x147)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
347 |
(let (($x16 (bvule (_ bv256 16) |$w|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
348 |
(let (($x17 (not $x16))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
349 |
(let (($x11 (=> (bvult |$w| (_ bv256 16)) (= (bvand |$w| (_ bv255 16)) |$w|)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
350 |
(let (($x12 (not $x11))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
351 |
(let ((?x39 ((_ extract 7 0) |$w|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
352 |
(let ((?x63 (concat (_ bv0 8) ?x39))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
353 |
(let (($x70 (= ?x63 |$w|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
354 |
(let (($x76 (or $x16 $x70))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
355 |
(let ((@x65 (monotonicity (rewrite (= (bvnot (_ bv255 8)) (_ bv0 8))) (rewrite (= (bvnot (bvnot ?x39)) ?x39)) (= (concat (bvnot (_ bv255 8)) (bvnot (bvnot ?x39))) ?x63)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
356 |
(let ((?x53 (concat (bvnot (_ bv255 8)) (bvnot (bvnot ?x39))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
357 |
(let ((?x20 (bvnot |$w|))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
358 |
(let ((?x22 (bvor ?x20 (bvnot (_ bv255 16))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
359 |
(let ((?x23 (bvnot ?x22))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
360 |
(let ((@x45 (monotonicity (rewrite (= ((_ extract 7 0) ?x20) (bvnot ?x39))) (= (concat (_ bv255 8) ((_ extract 7 0) ?x20)) (concat (_ bv255 8) (bvnot ?x39)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
361 |
(let ((@x31 (monotonicity (rewrite (= (bvnot (_ bv255 16)) (_ bv65280 16))) (= ?x22 (bvor ?x20 (_ bv65280 16)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
362 |
(let ((@x38 (trans @x31 (rewrite (= (bvor ?x20 (_ bv65280 16)) (concat (_ bv255 8) ((_ extract 7 0) ?x20)))) (= ?x22 (concat (_ bv255 8) ((_ extract 7 0) ?x20)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
363 |
(let ((@x50 (monotonicity (trans @x38 @x45 (= ?x22 (concat (_ bv255 8) (bvnot ?x39)))) (= ?x23 (bvnot (concat (_ bv255 8) (bvnot ?x39))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
364 |
(let ((@x57 (trans @x50 (rewrite (= (bvnot (concat (_ bv255 8) (bvnot ?x39))) ?x53)) (= ?x23 ?x53)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
365 |
(let ((@x69 (trans (rewrite (= (bvand |$w| (_ bv255 16)) ?x23)) (trans @x57 @x65 (= ?x23 ?x63)) (= (bvand |$w| (_ bv255 16)) ?x63)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
366 |
(let ((@x75 (monotonicity (rewrite (= (bvult |$w| (_ bv256 16)) $x17)) (monotonicity @x69 (= (= (bvand |$w| (_ bv255 16)) |$w|) $x70)) (= $x11 (=> $x17 $x70))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
367 |
(let ((@x83 (monotonicity (trans @x75 (rewrite (= (=> $x17 $x70) $x76)) (= $x11 $x76)) (= $x12 (not $x76))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
368 |
(let ((@x155 (mp (|not-or-elim| (mp (asserted $x12) @x83 (not $x76)) $x17) (monotonicity @x151 (= $x17 (not $x147))) (not $x147)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
369 |
(let (($x318 (= k!140 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
370 |
(let ((@x157 (|not-or-elim| @x155 (not (or k!140 $x137 (not (or $x138 (not $x137)))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
371 |
(let ((@x323 (mp (|not-or-elim| @x157 $x138) (symm (rewrite (= $x318 $x138)) (= $x138 $x318)) $x318))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
372 |
(let (($x324 (= k!130 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
373 |
(let ((@x329 (mp (|not-or-elim| (|not-or-elim| @x157 (not $x137)) $x133) (symm (rewrite (= $x324 $x133)) (= $x133 $x324)) $x324))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
374 |
(let (($x330 (= k!120 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
375 |
(let ((@x335 (mp (|not-or-elim| (|not-or-elim| (|not-or-elim| @x157 (not $x137)) $x134) $x128) (symm (rewrite (= $x330 $x128)) (= $x128 $x330)) $x330))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
376 |
(let (($x336 (= k!110 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
377 |
(let ((@x163 (|not-or-elim| (|not-or-elim| (|not-or-elim| @x157 (not $x137)) $x134) (not (or k!110 $x122 (not (or $x123 (not $x122)))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
378 |
(let ((@x341 (mp (|not-or-elim| @x163 $x123) (symm (rewrite (= $x336 $x123)) (= $x123 $x336)) $x336))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
379 |
(let (($x342 (= k!100 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
380 |
(let ((@x347 (mp (|not-or-elim| (|not-or-elim| @x163 (not $x122)) $x118) (symm (rewrite (= $x342 $x118)) (= $x118 $x342)) $x342))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
381 |
(let (($x348 (= k!90 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
382 |
(let ((@x352 (symm (rewrite (= $x348 (not k!90))) (= (not k!90) $x348)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
383 |
(let (($x113 (not k!90))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
384 |
(let ((@x353 (mp (|not-or-elim| (|not-or-elim| (|not-or-elim| @x163 (not $x122)) $x119) $x113) @x352 $x348))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
385 |
(let (($x354 (= k!80 false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
386 |
(let ((@x358 (symm (rewrite (= $x354 (not k!80))) (= (not k!80) $x354)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
387 |
(let (($x114 (not k!80))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
388 |
(let ((@x359 (mp (|not-or-elim| (|not-or-elim| (|not-or-elim| @x163 (not $x122)) $x119) $x114) @x358 $x354))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
389 |
(let ((@x363 (monotonicity @x359 @x353 @x347 @x341 @x335 @x329 @x323 (mp (|not-or-elim| @x155 $x143) @x316 $x312) $x362))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
390 |
(let (($x200 (not $x199))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
391 |
(let (($x205 (not $x200))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
392 |
(let ((?x191 (mkbv k!00 k!10 k!20 k!30 k!40 k!50 k!60 k!70 false false false false false false false false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
393 |
(let ((?x183 (mkbv k!00 k!10 k!20 k!30 k!40 k!50 k!60 k!70))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
394 |
(let ((?x188 (concat (mkbv false false false false false false false false) ?x183))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
395 |
(let ((@x187 (trans (monotonicity @x109 (= ?x39 ((_ extract 7 0) ?x107))) (rewrite (= ((_ extract 7 0) ?x107) ?x183)) (= ?x39 ?x183)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
396 |
(let (($x178 (= (_ bv0 8) (mkbv false false false false false false false false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
397 |
(let ((@x195 (trans (monotonicity (rewrite $x178) @x187 (= ?x63 ?x188)) (rewrite (= ?x188 ?x191)) (= ?x63 ?x191)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
398 |
(let ((@x204 (trans (monotonicity @x195 @x109 (= $x70 (= ?x191 ?x107))) (rewrite (= (= ?x191 ?x107) $x200)) (= $x70 $x200)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
399 |
(let ((@x208 (mp (|not-or-elim| (mp (asserted $x12) @x83 (not $x76)) (not $x70)) (monotonicity @x204 (= (not $x70) $x205)) $x205))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
400 |
(mp (mp @x208 (rewrite (= $x205 $x199)) $x199) (trans @x363 (rewrite $x364) (= $x199 false)) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
401 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
402 |
f611d24907b7d60f35d0adf911b0c146313d6c07 13 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
403 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
404 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
405 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
406 |
(let ((?x10 (|$p| true))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
407 |
(let (($x11 (= (|$p| (ite (bvule (_ bv0 4) |$a|) true false)) ?x10))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
408 |
(let (($x12 (not $x11))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
409 |
(let (($x8 (ite (bvule (_ bv0 4) |$a|) true false))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
410 |
(let ((@x20 (monotonicity (rewrite (= (bvule (_ bv0 4) |$a|) true)) (= $x8 (ite true true false))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
411 |
(let ((@x24 (trans @x20 (rewrite (= (ite true true false) true)) (= $x8 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
412 |
(let ((@x32 (trans (monotonicity (monotonicity @x24 $x11) (= $x11 (= ?x10 ?x10))) (rewrite (= (= ?x10 ?x10) true)) (= $x11 true)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
413 |
(let ((@x39 (trans (monotonicity @x32 (= $x12 (not true))) (rewrite (= (not true) false)) (= $x12 false)))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
414 |
(mp (asserted $x12) @x39 false))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
415 |
|
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
416 |
eb851e3355032ef6b75793abd314b6b2bc9c3459 18 0 |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
417 |
unsat |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
418 |
((set-logic <null>) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
419 |
(proof |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
420 |
(let (($x600 (forall ((?v0 (_ BitVec 2)) )(!(not (<= (|$bv2int| ?v0) 0)) :pattern ( (|$bv2int| ?v0) ))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
421 |
)) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
422 |
(let (($x45 (forall ((?v0 (_ BitVec 2)) )(not (<= (|$bv2int| ?v0) 0))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
423 |
)) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
424 |
(let ((@x602 (refl (= (not (<= (|$bv2int| ?0) 0)) (not (<= (|$bv2int| ?0) 0)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
425 |
(let ((@x132 (refl (|~| (not (<= (|$bv2int| ?0) 0)) (not (<= (|$bv2int| ?0) 0)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
426 |
(let (($x24 (forall ((?v0 (_ BitVec 2)) )(let ((?x22 (|$bv2int| ?v0))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
427 |
(< 0 ?x22))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
428 |
)) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
429 |
(let ((@x44 (rewrite (= (< 0 (|$bv2int| ?0)) (not (<= (|$bv2int| ?0) 0)))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
430 |
(let ((@x133 (|mp~| (mp (asserted $x24) (|quant-intro| @x44 (= $x24 $x45)) $x45) (|nnf-pos| @x132 (|~| $x45 $x45)) $x45))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
431 |
(let ((@x597 (|unit-resolution| ((_ |quant-inst| (_ bv0 2)) (or (not $x600) (not (<= (|$bv2int| (_ bv0 2)) 0)))) (mp @x133 (|quant-intro| @x602 (= $x45 $x600)) $x600) (not (<= (|$bv2int| (_ bv0 2)) 0))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
432 |
(let ((@x589 ((_ |th-lemma| arith triangle-eq) (or (not (= (|$bv2int| (_ bv0 2)) 0)) (<= (|$bv2int| (_ bv0 2)) 0))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
433 |
(|unit-resolution| @x589 (asserted (= (|$bv2int| (_ bv0 2)) 0)) @x597 false)))))))))))) |
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff
changeset
|
434 |