src/HOL/SMT_Examples/SMT_Word_Examples.certs2
author blanchet
Sun, 27 Jul 2014 21:20:11 +0200
changeset 57823 d1e9022c0175
parent 57204 7c36ce8e45f6
child 57711 caadd484dec6
permissions -rw-r--r--
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
     1
8e6fd56de8adc20c29f4bdb8c2c55e63988185a8 8 0
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
     2
unsat
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
     3
((set-logic <null>)
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
     4
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
     5
(let ((@x38 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
     6
(let ((@x42 (trans @x38 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
     7
(let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
     8
(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false))))))
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
     9
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    10
aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    14
(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    15
(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    16
(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    17
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    18
a14afea8a52a1586ff44eff03b88f1717144d17a 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    22
(let ((@x38 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    23
(let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    24
(mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x42 false)))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    25
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    26
282d94be68c87485ea9ec13e80f6f2a51b18f5bd 9 0
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
    27
unsat
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
    28
((set-logic <null>)
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
    29
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    30
(let ((@x38 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    31
(let ((@x42 (trans @x38 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    32
(let ((@x45 (monotonicity @x42 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    33
(let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    34
(mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x49 false)))))))
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
    35
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    36
4df99826f79b2c96079a4c58ea51a58b8cc6199c 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    40
(let ((@x38 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    41
(let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    42
(let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    43
(let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    44
(mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    45
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    46
6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    47
unsat
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    48
((set-logic <null>)
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    49
(proof
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    50
(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    51
(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    52
(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
    53
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    54
45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    55
unsat
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    56
((set-logic <null>)
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    57
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    58
(let ((@x43 (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))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    59
(let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    60
(let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    61
(let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    62
(mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    63
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    64
00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0
56111
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
    65
unsat
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
    66
((set-logic <null>)
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
    67
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    68
(let ((@x42 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    69
(let ((@x47 (trans @x42 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    70
(let ((@x52 (monotonicity @x47 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    71
(let ((@x56 (trans @x52 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    72
(let ((@x59 (monotonicity @x56 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    73
(let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    74
(mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false)))))))))
56111
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
    75
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    76
9673ca576ccae343db48aa68f876fd3a2515cc33 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    80
(let ((?x35 (bvadd b$ c$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    81
(let ((?x36 (bvadd ?x35 a$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    82
(let ((?x30 (bvmul (_ bv2 32) b$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    83
(let ((?x31 (bvadd a$ ?x30)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    84
(let ((?x33 (bvadd ?x31 c$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    85
(let ((?x34 (bvsub ?x33 b$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    86
(let (($x37 (= ?x34 ?x36)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    87
(let (($x38 (not $x37)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    88
(let ((@x58 (rewrite (= (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    89
(let ((@x48 (rewrite (= (bvsub (bvadd a$ ?x30 c$) b$) (bvadd a$ b$ c$)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    90
(let ((@x46 (monotonicity (rewrite (= ?x33 (bvadd a$ ?x30 c$))) (= ?x34 (bvsub (bvadd a$ ?x30 c$) b$)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    91
(let ((@x56 (monotonicity (trans @x46 @x48 (= ?x34 (bvadd a$ b$ c$))) (rewrite (= ?x36 (bvadd a$ b$ c$))) (= $x37 (= (bvadd a$ b$ c$) (bvadd a$ b$ c$))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    92
(let ((@x63 (monotonicity (trans @x56 @x58 (= $x37 true)) (= $x38 (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    93
(let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
    94
(mp (asserted $x38) @x67 false)))))))))))))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
    95
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
    96
b4600e6d14c88b633ac7bcc5b2e24af8539b0218 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   100
(let ((?x31 (bvmul (_ bv4 4) x$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   101
(let (($x32 (= ?x31 (_ bv4 4))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   102
(let (($x43 (= (_ bv5 4) x$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   103
(let (($x56 (not (or (not $x43) (= (_ bv4 4) ?x31)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   104
(let ((@x48 (monotonicity (rewrite (= (= x$ (_ bv5 4)) $x43)) (= (not (= x$ (_ bv5 4))) (not $x43)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   105
(let ((@x55 (monotonicity @x48 (rewrite (= $x32 (= (_ bv4 4) ?x31))) (= (or (not (= x$ (_ bv5 4))) $x32) (or (not $x43) (= (_ bv4 4) ?x31))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   106
(let (($x34 (not (=> (= x$ (_ bv5 4)) $x32))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   107
(let ((@x39 (rewrite (= (=> (= x$ (_ bv5 4)) $x32) (or (not (= x$ (_ bv5 4))) $x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   108
(let ((@x60 (trans (monotonicity @x39 (= $x34 (not (or (not (= x$ (_ bv5 4))) $x32)))) (monotonicity @x55 (= (not (or (not (= x$ (_ bv5 4))) $x32)) $x56)) (= $x34 $x56))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   109
(let ((@x67 (monotonicity (not-or-elim (mp (asserted $x34) @x60 $x56) $x43) (= ?x31 (bvmul (_ bv4 4) (_ bv5 4))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   110
(let ((@x73 (monotonicity (trans @x67 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x32) (= (= (_ bv4 4) ?x31) (= (_ bv4 4) (_ bv4 4))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   111
(let ((@x77 (trans @x73 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x31) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   112
(let ((@x84 (trans (monotonicity @x77 (= (not (= (_ bv4 4) ?x31)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x31)) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   113
(mp (not-or-elim (mp (asserted $x34) @x60 $x56) (not (= (_ bv4 4) ?x31))) @x84 false))))))))))))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   114
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   115
d150015a66b6757a72346710966844993c0f3c27 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   119
(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   120
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   121
(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   122
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   123
(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   124
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   125
200e29aa9f19844d244c5c9755155eb956c5cf7c 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   129
(let ((@x37 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   130
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   131
(let ((@x44 (monotonicity @x41 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   132
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   133
(mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   134
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   135
d7cc0827eb340c29b0f489145022e4b3e3610818 9 0
56111
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   136
unsat
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   137
((set-logic <null>)
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   138
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   139
(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   140
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   141
(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   142
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   143
(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
56111
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   144
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   145
14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   149
(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   150
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   151
(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   152
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   153
(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   154
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   155
3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   156
unsat
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   157
((set-logic <null>)
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   158
(proof
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   159
(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   160
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   161
(let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   162
(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   163
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   164
8d29c9b5ef712a3d9d2db87383c9c25c0b553e01 8 0
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   165
unsat
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   166
((set-logic <null>)
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   167
(proof
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   168
(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   169
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   170
(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))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   171
(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   172
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   173
880bee16a8f6469b14122277b92e87533ef6a071 9 0
57170
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   174
unsat
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   175
((set-logic <null>)
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   176
(proof
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   177
(let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10))))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   178
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   179
(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true)))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   180
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   181
(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   182
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   183
446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   187
(let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   188
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   189
(let ((@x43 (monotonicity @x40 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   190
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   191
(mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   192
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   193
956d8b6229140c8c4aa869ab0f3765697ab8ff25 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   197
(let ((@x36 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   198
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   199
(let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   200
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   201
(mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   202
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   203
8e075e24ee51b2c8d282203ef406cf993a4d32e8 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   207
(let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   208
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   209
(let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   210
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   211
(mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   212
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   213
e11f6641dec327aa96166093ca6eb62aa10965c0 9 0
57170
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   214
unsat
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   215
((set-logic <null>)
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   216
(proof
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   217
(let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8))))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   218
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   219
(let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true)))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   220
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   221
(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
3afada8f820d updated SMT2 certificates
blanchet
parents: 56727
diff changeset
   222
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   223
f1f29c69ebfcb6af36e96ba5a738d9b0d7b31835 9 0
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
   224
unsat
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
   225
((set-logic <null>)
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
   226
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   227
(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   228
(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   229
(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   230
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   231
(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
   232
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   233
d5599ccc28266367053026b485d411472eb0665c 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
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   237
(let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   238
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   239
(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   240
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   241
(mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false)))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   242
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   243
5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   244
unsat
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   245
((set-logic <null>)
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   246
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   247
(let ((?x31 (bvand x$ (_ bv255 16))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   248
(let ((?x29 (bvand x$ (_ bv65280 16))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   249
(let ((?x32 (bvor ?x29 ?x31)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   250
(let (($x33 (= ?x32 x$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   251
(let (($x34 (not $x33)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   252
(let ((@x59 (symm (commutativity (= (= x$ ?x32) $x33)) (= $x33 (= x$ ?x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   253
(let ((@x35 (asserted $x34)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   254
(let ((@x63 (mp @x35 (monotonicity @x59 (= $x34 (not (= x$ ?x32)))) (not (= x$ ?x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   255
(let (($x52 (= x$ ?x32)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   256
(let ((@x26 (true-axiom true)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   257
(let (($x53 (or $x52 false false false false false false false false false false false false false false false false)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   258
(let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   259
(unit-resolution @x55 @x63 false)))))))))))))))
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   260
57823
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   261
33a52e620069e1ecebbc00aa6b0099170558c111 9 0
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   262
unsat
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   263
((set-logic <null>)
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   264
(proof
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   265
(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   266
(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   267
(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true)))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   268
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   269
(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false)))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   270
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   271
115ab22c9945d493b971e69a38d9e608c5b40a71 29 0
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   272
unsat
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   273
((set-logic <null>)
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   274
(proof
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   275
(let ((?x28 (bv2int$ (_ bv0 2))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   276
(let (($x183 (<= ?x28 0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   277
(let (($x184 (not $x183)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   278
(let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   279
(let (($x53 (<= ?x47 0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   280
(not $x53))) :pattern ( (bv2int$ ?v0) )))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   281
))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   282
(let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   283
(let (($x53 (<= ?x47 0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   284
(not $x53))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   285
))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   286
(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   287
(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   288
(let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   289
(< 0 ?x47)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   290
))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   291
(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   292
(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   293
(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   294
(let (($x187 (not $x175)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   295
(let (($x188 (or $x187 $x184)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   296
(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   297
(let (($x29 (= ?x28 0)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   298
(let ((@x30 (asserted $x29)))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   299
(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false)))))))))))))))))))
d1e9022c0175 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57204
diff changeset
   300
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   301
1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0
56079
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   302
unsat
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   303
((set-logic <null>)
175ac95720d4 use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
diff changeset
   304
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   305
(let ((?x31 (bvand w$ (_ bv255 16))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   306
(let (($x32 (= ?x31 w$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   307
(let (($x64 (not $x32)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   308
(let ((@x318 (symm (commutativity (= (= w$ ?x31) $x32)) (= $x32 (= w$ ?x31)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   309
(let (($x57 (not (or (bvule (_ bv256 16) w$) $x32))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   310
(let ((@x49 (monotonicity (rewrite (= (bvult w$ (_ bv256 16)) (not (bvule (_ bv256 16) w$)))) (= (not (bvult w$ (_ bv256 16))) (not (not (bvule (_ bv256 16) w$)))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   311
(let ((@x53 (trans @x49 (rewrite (= (not (not (bvule (_ bv256 16) w$))) (bvule (_ bv256 16) w$))) (= (not (bvult w$ (_ bv256 16))) (bvule (_ bv256 16) w$)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   312
(let ((@x56 (monotonicity @x53 (= (or (not (bvult w$ (_ bv256 16))) $x32) (or (bvule (_ bv256 16) w$) $x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   313
(let ((@x59 (monotonicity @x56 (= (not (or (not (bvult w$ (_ bv256 16))) $x32)) $x57))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   314
(let (($x34 (not (=> (bvult w$ (_ bv256 16)) $x32))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   315
(let ((@x39 (rewrite (= (=> (bvult w$ (_ bv256 16)) $x32) (or (not (bvult w$ (_ bv256 16))) $x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   316
(let ((@x42 (monotonicity @x39 (= $x34 (not (or (not (bvult w$ (_ bv256 16))) $x32))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   317
(let ((@x65 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x64)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   318
(let ((@x322 (mp @x65 (monotonicity @x318 (= $x64 (not (= w$ ?x31)))) (not (= w$ ?x31)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   319
(let (($x300 (= w$ ?x31)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   320
(let (($x81 (= ((_ extract 15 15) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   321
(let (($x264 (not $x81)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   322
(let (($x74 (= ((_ extract 8 8) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   323
(let (($x75 (= ((_ extract 9 9) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   324
(let (($x82 (and $x75 $x74)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   325
(let (($x83 (or $x75 $x74 $x82)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   326
(let (($x76 (= ((_ extract 10 10) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   327
(let (($x84 (and $x76 $x83)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   328
(let (($x85 (or $x76 $x75 $x74 $x82 $x84)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   329
(let (($x77 (= ((_ extract 11 11) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   330
(let (($x86 (and $x77 $x85)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   331
(let (($x87 (or $x77 $x76 $x75 $x74 $x82 $x84 $x86)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   332
(let (($x78 (= ((_ extract 12 12) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   333
(let (($x88 (and $x78 $x87)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   334
(let (($x89 (or $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   335
(let (($x79 (= ((_ extract 13 13) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   336
(let (($x90 (and $x79 $x89)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   337
(let (($x91 (or $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   338
(let (($x80 (= ((_ extract 14 14) w$) (_ bv1 1))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   339
(let (($x92 (and $x80 $x91)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   340
(let (($x93 (or $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   341
(let (($x94 (and $x81 $x93)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   342
(let (($x95 (or $x81 $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92 $x94)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   343
(let (($x297 (not $x95)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   344
(let (($x43 (bvule (_ bv256 16) w$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   345
(let (($x44 (not $x43)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   346
(let ((@x63 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x44)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   347
(let ((@x303 (unit-resolution ((_ th-lemma bv) (or $x43 $x297)) @x63 $x297)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   348
(let ((@x26 (true-axiom true)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   349
(let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   350
(let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   351
(unit-resolution @x314 @x322 false)))))))))))))))))))))))))))))))))))))))))))))))))
56111
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   352
57204
7c36ce8e45f6 updated Z3 certificates
blanchet
parents: 57170
diff changeset
   353
d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0
56111
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   354
unsat
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   355
((set-logic <null>)
5b76e1790c38 updated SMT2 certificates
blanchet
parents: 56109
diff changeset
   356
(proof
56727
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   357
(let ((?x32 (p$ true)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   358
(let (($x29 (bvule (_ bv0 4) a$)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   359
(let (($x30 (ite $x29 true false)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   360
(let ((?x31 (p$ $x30)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   361
(let (($x33 (= ?x31 ?x32)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   362
(let (($x34 (not $x33)))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   363
(let ((@x52 (monotonicity (monotonicity (rewrite (= $x29 true)) (= (p$ $x29) ?x32)) (= (= (p$ $x29) ?x32) (= ?x32 ?x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   364
(let ((@x56 (trans @x52 (rewrite (= (= ?x32 ?x32) true)) (= (= (p$ $x29) ?x32) true))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   365
(let ((@x63 (trans (monotonicity @x56 (= (not (= (p$ $x29) ?x32)) (not true))) (rewrite (= (not true) false)) (= (not (= (p$ $x29) ?x32)) false))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   366
(let ((@x43 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= ?x31 (p$ $x29))) (= $x33 (= (p$ $x29) ?x32)))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   367
(let ((@x46 (monotonicity @x43 (= $x34 (not (= (p$ $x29) ?x32))))))
75f4fdafb285 use Z3 4.3.2 to fix most FIXMEs
blanchet
parents: 56111
diff changeset
   368
(mp (asserted $x34) (trans @x46 @x63 (= $x34 false)) false))))))))))))))
56109
1ba56358eba4 updated SMT example certificates
blanchet
parents: 56079
diff changeset
   369