updated SMT certificates
authorblanchet
Mon Nov 24 12:35:13 2014 +0100 (2014-11-24)
changeset 59046db5a718e8c09
parent 59045 1da9b8045026
child 59047 8d7cec9b861d
updated SMT certificates
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Word_Examples.certs
src/HOL/SMT_Examples/VCC_Max.certs
     1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Nov 24 12:35:13 2014 +0100
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Nov 24 12:35:13 2014 +0100
     1.3 @@ -951,6 +951,14 @@
     1.4  (let ((@x211 ((_ quant-inst c$) $x549)))
     1.5  (unit-resolution @x211 @x199 (unit-resolution @x592 @x199 $x584) false)))))))))))))))))))))))))))))))))))))))
     1.6  
     1.7 +1b3bdde0d609ebf7ad7472d1510134c9c367d283 7 0
     1.8 +unsat
     1.9 +((set-logic AUFLIA)
    1.10 +(proof
    1.11 +(let ((@x35 (monotonicity (rewrite (= (= 3 3) true)) (= (not (= 3 3)) (not true)))))
    1.12 +(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= 3 3)) false))))
    1.13 +(mp (asserted (not (= 3 3))) @x39 false)))))
    1.14 +
    1.15  ee1b9a27124d1797593a214fc9b1585b73aca864 26 0
    1.16  unsat
    1.17  ((set-logic AUFLIA)
    1.18 @@ -978,14 +986,6 @@
    1.19  (let ((@x70 ((_ quant-inst x$) $x156)))
    1.20  (unit-resolution @x70 @x491 @x49 false)))))))))))))))))))
    1.21  
    1.22 -1b3bdde0d609ebf7ad7472d1510134c9c367d283 7 0
    1.23 -unsat
    1.24 -((set-logic AUFLIA)
    1.25 -(proof
    1.26 -(let ((@x35 (monotonicity (rewrite (= (= 3 3) true)) (= (not (= 3 3)) (not true)))))
    1.27 -(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= 3 3)) false))))
    1.28 -(mp (asserted (not (= 3 3))) @x39 false)))))
    1.29 -
    1.30  a90c5a0ce94c691b0e4756f87e5d5fdbfd876893 7 0
    1.31  unsat
    1.32  ((set-logic AUFLIRA)
    1.33 @@ -1187,26 +1187,6 @@
    1.34  (let ((@x57 (trans @x53 (rewrite (= (not true) false)) (= (not (not (= (+ 2 2) 5))) false))))
    1.35  (mp (asserted (not (not (= (+ 2 2) 5)))) @x57 false)))))))))
    1.36  
    1.37 -dfbbe6f3879b3c49e6d5f7ecff4f8f81ed746bd4 19 0
    1.38 -unsat
    1.39 -((set-logic AUFLIRA)
    1.40 -(proof
    1.41 -(let ((?x32 (* 7.0 a$)))
    1.42 -(let ((?x29 (* 3.0 x$)))
    1.43 -(let ((?x33 (+ ?x29 ?x32)))
    1.44 -(let (($x43 (>= ?x33 4.0)))
    1.45 -(let (($x41 (not $x43)))
    1.46 -(let ((@x40 (mp (asserted (< ?x33 4.0)) (rewrite (= (< ?x33 4.0) $x41)) $x41)))
    1.47 -(let ((?x38 (* 2.0 x$)))
    1.48 -(let (($x48 (<= ?x38 3.0)))
    1.49 -(let (($x49 (not $x48)))
    1.50 -(let ((@x52 (mp (asserted (< 3.0 ?x38)) (rewrite (= (< 3.0 ?x38) $x49)) $x49)))
    1.51 -(let (($x58 (>= a$ 0.0)))
    1.52 -(let ((@x62 (monotonicity (rewrite (= (< a$ 0.0) (not $x58))) (= (not (< a$ 0.0)) (not (not $x58))))))
    1.53 -(let ((@x66 (trans @x62 (rewrite (= (not (not $x58)) $x58)) (= (not (< a$ 0.0)) $x58))))
    1.54 -(let ((@x67 (mp (asserted (not (< a$ 0.0))) @x66 $x58)))
    1.55 -((_ th-lemma arith farkas 7 3/2 1) @x67 @x52 @x40 false)))))))))))))))))
    1.56 -
    1.57  3a6df2b095b936aac9a1d533e306f2d31b4fb44e 22 0
    1.58  unsat
    1.59  ((set-logic AUFLIA)
    1.60 @@ -1230,6 +1210,26 @@
    1.61  (let ((@x78 (trans (monotonicity @x71 (= $x40 (not true))) (rewrite (= (not true) false)) (= $x40 false))))
    1.62  (mp (asserted $x40) @x78 false))))))))))))))))))))
    1.63  
    1.64 +dfbbe6f3879b3c49e6d5f7ecff4f8f81ed746bd4 19 0
    1.65 +unsat
    1.66 +((set-logic AUFLIRA)
    1.67 +(proof
    1.68 +(let ((?x32 (* 7.0 a$)))
    1.69 +(let ((?x29 (* 3.0 x$)))
    1.70 +(let ((?x33 (+ ?x29 ?x32)))
    1.71 +(let (($x43 (>= ?x33 4.0)))
    1.72 +(let (($x41 (not $x43)))
    1.73 +(let ((@x40 (mp (asserted (< ?x33 4.0)) (rewrite (= (< ?x33 4.0) $x41)) $x41)))
    1.74 +(let ((?x38 (* 2.0 x$)))
    1.75 +(let (($x48 (<= ?x38 3.0)))
    1.76 +(let (($x49 (not $x48)))
    1.77 +(let ((@x52 (mp (asserted (< 3.0 ?x38)) (rewrite (= (< 3.0 ?x38) $x49)) $x49)))
    1.78 +(let (($x58 (>= a$ 0.0)))
    1.79 +(let ((@x62 (monotonicity (rewrite (= (< a$ 0.0) (not $x58))) (= (not (< a$ 0.0)) (not (not $x58))))))
    1.80 +(let ((@x66 (trans @x62 (rewrite (= (not (not $x58)) $x58)) (= (not (< a$ 0.0)) $x58))))
    1.81 +(let ((@x67 (mp (asserted (not (< a$ 0.0))) @x66 $x58)))
    1.82 +((_ th-lemma arith farkas 7 3/2 1) @x67 @x52 @x40 false)))))))))))))))))
    1.83 +
    1.84  7d3773a9d63ce2ada82ac001b84291cdc85d7ab8 159 0
    1.85  unsat
    1.86  ((set-logic AUFLIA)
    1.87 @@ -3538,43 +3538,10 @@
    1.88  (let ((@x125 (mp (mp @x110 (quant-intro @x115 (= $x107 $x116)) $x116) (quant-intro (rewrite (= $x113 $x104)) (= $x116 $x122)) $x122)))
    1.89  (mp (mp @x125 @x156 $x152) @x180 false))))))))))))))))))))))))))))))))))))))))))))))
    1.90  
    1.91 -79a22a7943e8703e97ab2cddee03d311bc7ae2a6 36 0
    1.92 -unsat
    1.93 -((set-logic AUFLIA)
    1.94 -(proof
    1.95 -(let (($x35 (forall ((?v0 Int) )(let ((?x32 (* 2 a$)))
    1.96 -(let ((?x31 (* 2 ?v0)))
    1.97 -(let (($x33 (< ?x31 ?x32)))
    1.98 -(let (($x29 (< ?v0 a$)))
    1.99 -(=> $x29 $x33))))))
   1.100 -))
   1.101 -(let (($x36 (not $x35)))
   1.102 -(let (($x42 (forall ((?v0 Int) )(let ((?x32 (* 2 a$)))
   1.103 -(let ((?x31 (* 2 ?v0)))
   1.104 -(let (($x33 (< ?x31 ?x32)))
   1.105 -(let (($x29 (< ?v0 a$)))
   1.106 -(let (($x38 (not $x29)))
   1.107 -(or $x38 $x33)))))))
   1.108 -))
   1.109 -(let (($x45 (not $x42)))
   1.110 -(let (($x71 (forall ((?v0 Int) )true)
   1.111 -))
   1.112 -(let ((?x32 (* 2 a$)))
   1.113 -(let ((?x31 (* 2 ?0)))
   1.114 -(let (($x33 (< ?x31 ?x32)))
   1.115 -(let (($x29 (< ?0 a$)))
   1.116 -(let (($x38 (not $x29)))
   1.117 -(let (($x39 (or $x38 $x33)))
   1.118 -(let (($x50 (>= (+ ?0 (* (- 1) a$)) 0)))
   1.119 -(let (($x49 (not $x50)))
   1.120 -(let ((@x61 (trans (monotonicity (rewrite (= $x29 $x49)) (= $x38 (not $x49))) (rewrite (= (not $x49) $x50)) (= $x38 $x50))))
   1.121 -(let ((@x66 (monotonicity @x61 (rewrite (= $x33 $x49)) (= $x39 (or $x50 $x49)))))
   1.122 -(let ((@x73 (quant-intro (trans @x66 (rewrite (= (or $x50 $x49) true)) (= $x39 true)) (= $x42 $x71))))
   1.123 -(let ((@x80 (monotonicity (trans @x73 (elim-unused (= $x71 true)) (= $x42 true)) (= $x45 (not true)))))
   1.124 -(let ((@x84 (trans @x80 (rewrite (= (not true) false)) (= $x45 false))))
   1.125 -(let ((@x47 (monotonicity (quant-intro (rewrite (= (=> $x29 $x33) $x39)) (= $x35 $x42)) (= $x36 $x45))))
   1.126 -(mp (asserted $x36) (trans @x47 @x84 (= $x36 false)) false))))))))))))))))))))))
   1.127 -
   1.128 +68af267a155ec93a64652d04b7ee09ecad3d48b9 3 0
   1.129 +(error "line 5 column 91: invalid function application, arguments missing")
   1.130 +sat
   1.131 +(error "line 7 column 10: proof is not available")
   1.132  ae4f4fb9c10608b8e3b893cc6c99e3ec5d13a86c 24 0
   1.133  unsat
   1.134  ((set-logic AUFLIA)
   1.135 @@ -3944,22 +3911,7 @@
   1.136  (let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
   1.137  (mp (asserted $x33) @x53 false)))))))))))
   1.138  
   1.139 -8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0
   1.140 -unsat
   1.141 -((set-logic AUFLIA)
   1.142 -(proof
   1.143 -(let (($x29 (forall ((?v0 A$) )(g$ ?v0))
   1.144 -))
   1.145 -(let (($x30 (ite $x29 true false)))
   1.146 -(let (($x31 (f$ $x30)))
   1.147 -(let (($x32 (=> $x31 true)))
   1.148 -(let (($x33 (not $x32)))
   1.149 -(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
   1.150 -(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
   1.151 -(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
   1.152 -(mp (asserted $x33) @x53 false)))))))))))
   1.153 -
   1.154 -b221de9d8dbe279344ac85e2ada07f5722636ce5 46 0
   1.155 +feaa6ef662dd489cf55f86209489c2992ff08d28 46 0
   1.156  unsat
   1.157  ((set-logic AUFLIA)
   1.158  (proof
   1.159 @@ -4006,7 +3958,34 @@
   1.160  (let ((@x478 (mp ((_ quant-inst 3 42) (or (not $x52) $x171)) (trans (monotonicity @x131 $x137) (rewrite (= $x134 $x134)) $x137) $x134)))
   1.161  (unit-resolution (unit-resolution @x478 @x78 $x168) (mp @x77 @x472 (not $x168)) false)))))))))))))))))))))))))))))))))))
   1.162  
   1.163 -5d3ccbcf168a634cad3952ad8f6d2798329d6a77 75 0
   1.164 +8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0
   1.165 +unsat
   1.166 +((set-logic AUFLIA)
   1.167 +(proof
   1.168 +(let (($x29 (forall ((?v0 A$) )(g$ ?v0))
   1.169 +))
   1.170 +(let (($x30 (ite $x29 true false)))
   1.171 +(let (($x31 (f$ $x30)))
   1.172 +(let (($x32 (=> $x31 true)))
   1.173 +(let (($x33 (not $x32)))
   1.174 +(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
   1.175 +(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
   1.176 +(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
   1.177 +(mp (asserted $x33) @x53 false)))))))))))
   1.178 +
   1.179 +40c61a0200976d6203302a7343af5b7ad1e6ce36 11 0
   1.180 +unsat
   1.181 +((set-logic AUFLIA)
   1.182 +(proof
   1.183 +(let (($x29 (forall ((?v0 A$) )(p$ ?v0))
   1.184 +))
   1.185 +(let (($x30 (not $x29)))
   1.186 +(let (($x31 (or $x29 $x30)))
   1.187 +(let (($x32 (not $x31)))
   1.188 +(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
   1.189 +(mp (asserted $x32) @x42 false))))))))
   1.190 +
   1.191 +9cdd1051dbf4e0648f71536fbc74bbab8e0e744e 75 0
   1.192  unsat
   1.193  ((set-logic AUFLIA)
   1.194  (proof
   1.195 @@ -4082,18 +4061,6 @@
   1.196  (let ((@x82 (asserted $x81)))
   1.197  (unit-resolution @x82 @x466 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   1.198  
   1.199 -40c61a0200976d6203302a7343af5b7ad1e6ce36 11 0
   1.200 -unsat
   1.201 -((set-logic AUFLIA)
   1.202 -(proof
   1.203 -(let (($x29 (forall ((?v0 A$) )(p$ ?v0))
   1.204 -))
   1.205 -(let (($x30 (not $x29)))
   1.206 -(let (($x31 (or $x29 $x30)))
   1.207 -(let (($x32 (not $x31)))
   1.208 -(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
   1.209 -(mp (asserted $x32) @x42 false))))))))
   1.210 -
   1.211  f17a5e4d5f1a5a93fbc847f858c7c845c29d8349 109 0
   1.212  unsat
   1.213  ((set-logic AUFLIA)
   1.214 @@ -4204,7 +4171,7 @@
   1.215  (let ((@x81 (asserted $x80)))
   1.216  (unit-resolution @x81 (trans @x397 ((_ th-lemma arith eq-propagate 1 1 -4 -4) @x410 @x422 @x428 @x438 (= ?x490 6)) $x79) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   1.217  
   1.218 -16cd6b3ca7edac6486d6ca7a72e97f4ad1c07e37 336 0
   1.219 +8c0c900f4d4a92edc7d6113704948dc9280df015 336 0
   1.220  unsat
   1.221  ((set-logic <null>)
   1.222  (proof
   1.223 @@ -4541,7 +4508,7 @@
   1.224  (let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
   1.225  (unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   1.226  
   1.227 -d277a40ca34ecc409672601e981711fef2d0064f 64 0
   1.228 +db184ed715734759b60f9bdc99290a92283563f5 64 0
   1.229  unsat
   1.230  ((set-logic AUFLIA)
   1.231  (proof
     2.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Nov 24 12:35:13 2014 +0100
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Nov 24 12:35:13 2014 +0100
     2.3 @@ -354,9 +354,6 @@
     2.4  lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt
     2.5  lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt
     2.6  lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
     2.7 -lemma "\<forall>x::int.
     2.8 -  SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat x) SMT.Symb_Nil) SMT.Symb_Nil)
     2.9 -    (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
    2.10  lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt
    2.11  
    2.12  
     3.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs	Mon Nov 24 12:35:13 2014 +0100
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs	Mon Nov 24 12:35:13 2014 +0100
     3.3 @@ -1,11 +1,3 @@
     3.4 -aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0
     3.5 -unsat
     3.6 -((set-logic <null>)
     3.7 -(proof
     3.8 -(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
     3.9 -(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
    3.10 -(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
    3.11 -
    3.12  8e6fd56de8adc20c29f4bdb8c2c55e63988185a8 8 0
    3.13  unsat
    3.14  ((set-logic <null>)
    3.15 @@ -15,6 +7,14 @@
    3.16  (let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
    3.17  (mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false))))))
    3.18  
    3.19 +aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0
    3.20 +unsat
    3.21 +((set-logic <null>)
    3.22 +(proof
    3.23 +(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
    3.24 +(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
    3.25 +(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
    3.26 +
    3.27  a14afea8a52a1586ff44eff03b88f1717144d17a 7 0
    3.28  unsat
    3.29  ((set-logic <null>)
    3.30 @@ -43,14 +43,6 @@
    3.31  (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
    3.32  (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false)))))))
    3.33  
    3.34 -6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
    3.35 -unsat
    3.36 -((set-logic <null>)
    3.37 -(proof
    3.38 -(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
    3.39 -(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
    3.40 -(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
    3.41 -
    3.42  45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0
    3.43  unsat
    3.44  ((set-logic <null>)
    3.45 @@ -61,6 +53,14 @@
    3.46  (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
    3.47  (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false)))))))
    3.48  
    3.49 +6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
    3.50 +unsat
    3.51 +((set-logic <null>)
    3.52 +(proof
    3.53 +(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
    3.54 +(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
    3.55 +(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
    3.56 +
    3.57  00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0
    3.58  unsat
    3.59  ((set-logic <null>)
    3.60 @@ -73,16 +73,6 @@
    3.61  (let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false))))
    3.62  (mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false)))))))))
    3.63  
    3.64 -d150015a66b6757a72346710966844993c0f3c27 9 0
    3.65 -unsat
    3.66 -((set-logic <null>)
    3.67 -(proof
    3.68 -(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32))))))
    3.69 -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true))))
    3.70 -(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true)))))
    3.71 -(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false))))
    3.72 -(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false)))))))
    3.73 -
    3.74  b4600e6d14c88b633ac7bcc5b2e24af8539b0218 18 0
    3.75  unsat
    3.76  ((set-logic <null>)
    3.77 @@ -122,15 +112,15 @@
    3.78  (let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false))))
    3.79  (mp (asserted $x38) @x67 false)))))))))))))))))
    3.80  
    3.81 -d7cc0827eb340c29b0f489145022e4b3e3610818 9 0
    3.82 +d150015a66b6757a72346710966844993c0f3c27 9 0
    3.83  unsat
    3.84  ((set-logic <null>)
    3.85  (proof
    3.86 -(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
    3.87 -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
    3.88 -(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
    3.89 -(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
    3.90 -(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
    3.91 +(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32))))))
    3.92 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true))))
    3.93 +(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true)))))
    3.94 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false))))
    3.95 +(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false)))))))
    3.96  
    3.97  200e29aa9f19844d244c5c9755155eb956c5cf7c 9 0
    3.98  unsat
    3.99 @@ -142,6 +132,16 @@
   3.100  (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false))))
   3.101  (mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false)))))))
   3.102  
   3.103 +d7cc0827eb340c29b0f489145022e4b3e3610818 9 0
   3.104 +unsat
   3.105 +((set-logic <null>)
   3.106 +(proof
   3.107 +(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
   3.108 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
   3.109 +(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
   3.110 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
   3.111 +(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
   3.112 +
   3.113  3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0
   3.114  unsat
   3.115  ((set-logic <null>)
   3.116 @@ -151,6 +151,16 @@
   3.117  (let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
   3.118  (mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
   3.119  
   3.120 +14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0
   3.121 +unsat
   3.122 +((set-logic <null>)
   3.123 +(proof
   3.124 +(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
   3.125 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
   3.126 +(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
   3.127 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
   3.128 +(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
   3.129 +
   3.130  880bee16a8f6469b14122277b92e87533ef6a071 9 0
   3.131  unsat
   3.132  ((set-logic <null>)
   3.133 @@ -161,16 +171,6 @@
   3.134  (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
   3.135  (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
   3.136  
   3.137 -14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0
   3.138 -unsat
   3.139 -((set-logic <null>)
   3.140 -(proof
   3.141 -(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
   3.142 -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
   3.143 -(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
   3.144 -(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
   3.145 -(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
   3.146 -
   3.147  b48f55cefc567df166d8e9967c53372c30620183 8 0
   3.148  unsat
   3.149  ((set-logic <null>)
     4.1 --- a/src/HOL/SMT_Examples/VCC_Max.certs	Mon Nov 24 12:35:13 2014 +0100
     4.2 +++ b/src/HOL/SMT_Examples/VCC_Max.certs	Mon Nov 24 12:35:13 2014 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -05a761f33f246f0fee720bec6f015ca5aba01c4d 2972 0
     4.5 +8ec9d30fc9fdbc0ea292e0fdf148a6230c16dbca 2972 0
     4.6  unsat
     4.7  ((set-logic <null>)
     4.8  (declare-fun ?v0!14 () Int)