# HG changeset patch # User blanchet # Date 1416828913 -3600 # Node ID db5a718e8c098450a41adbfc594ba7c2b71b79c9 # Parent 1da9b8045026bf923aef3f4906e76c1dcb731448 updated SMT certificates diff -r 1da9b8045026 -r db5a718e8c09 src/HOL/SMT_Examples/SMT_Examples.certs --- a/src/HOL/SMT_Examples/SMT_Examples.certs Mon Nov 24 12:35:13 2014 +0100 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs Mon Nov 24 12:35:13 2014 +0100 @@ -951,6 +951,14 @@ (let ((@x211 ((_ quant-inst c$) $x549))) (unit-resolution @x211 @x199 (unit-resolution @x592 @x199 $x584) false))))))))))))))))))))))))))))))))))))))) +1b3bdde0d609ebf7ad7472d1510134c9c367d283 7 0 +unsat +((set-logic AUFLIA) +(proof +(let ((@x35 (monotonicity (rewrite (= (= 3 3) true)) (= (not (= 3 3)) (not true))))) +(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= 3 3)) false)))) +(mp (asserted (not (= 3 3))) @x39 false))))) + ee1b9a27124d1797593a214fc9b1585b73aca864 26 0 unsat ((set-logic AUFLIA) @@ -978,14 +986,6 @@ (let ((@x70 ((_ quant-inst x$) $x156))) (unit-resolution @x70 @x491 @x49 false))))))))))))))))))) -1b3bdde0d609ebf7ad7472d1510134c9c367d283 7 0 -unsat -((set-logic AUFLIA) -(proof -(let ((@x35 (monotonicity (rewrite (= (= 3 3) true)) (= (not (= 3 3)) (not true))))) -(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= 3 3)) false)))) -(mp (asserted (not (= 3 3))) @x39 false))))) - a90c5a0ce94c691b0e4756f87e5d5fdbfd876893 7 0 unsat ((set-logic AUFLIRA) @@ -1187,26 +1187,6 @@ (let ((@x57 (trans @x53 (rewrite (= (not true) false)) (= (not (not (= (+ 2 2) 5))) false)))) (mp (asserted (not (not (= (+ 2 2) 5)))) @x57 false))))))))) -dfbbe6f3879b3c49e6d5f7ecff4f8f81ed746bd4 19 0 -unsat -((set-logic AUFLIRA) -(proof -(let ((?x32 (* 7.0 a$))) -(let ((?x29 (* 3.0 x$))) -(let ((?x33 (+ ?x29 ?x32))) -(let (($x43 (>= ?x33 4.0))) -(let (($x41 (not $x43))) -(let ((@x40 (mp (asserted (< ?x33 4.0)) (rewrite (= (< ?x33 4.0) $x41)) $x41))) -(let ((?x38 (* 2.0 x$))) -(let (($x48 (<= ?x38 3.0))) -(let (($x49 (not $x48))) -(let ((@x52 (mp (asserted (< 3.0 ?x38)) (rewrite (= (< 3.0 ?x38) $x49)) $x49))) -(let (($x58 (>= a$ 0.0))) -(let ((@x62 (monotonicity (rewrite (= (< a$ 0.0) (not $x58))) (= (not (< a$ 0.0)) (not (not $x58)))))) -(let ((@x66 (trans @x62 (rewrite (= (not (not $x58)) $x58)) (= (not (< a$ 0.0)) $x58)))) -(let ((@x67 (mp (asserted (not (< a$ 0.0))) @x66 $x58))) -((_ th-lemma arith farkas 7 3/2 1) @x67 @x52 @x40 false))))))))))))))))) - 3a6df2b095b936aac9a1d533e306f2d31b4fb44e 22 0 unsat ((set-logic AUFLIA) @@ -1230,6 +1210,26 @@ (let ((@x78 (trans (monotonicity @x71 (= $x40 (not true))) (rewrite (= (not true) false)) (= $x40 false)))) (mp (asserted $x40) @x78 false)))))))))))))))))))) +dfbbe6f3879b3c49e6d5f7ecff4f8f81ed746bd4 19 0 +unsat +((set-logic AUFLIRA) +(proof +(let ((?x32 (* 7.0 a$))) +(let ((?x29 (* 3.0 x$))) +(let ((?x33 (+ ?x29 ?x32))) +(let (($x43 (>= ?x33 4.0))) +(let (($x41 (not $x43))) +(let ((@x40 (mp (asserted (< ?x33 4.0)) (rewrite (= (< ?x33 4.0) $x41)) $x41))) +(let ((?x38 (* 2.0 x$))) +(let (($x48 (<= ?x38 3.0))) +(let (($x49 (not $x48))) +(let ((@x52 (mp (asserted (< 3.0 ?x38)) (rewrite (= (< 3.0 ?x38) $x49)) $x49))) +(let (($x58 (>= a$ 0.0))) +(let ((@x62 (monotonicity (rewrite (= (< a$ 0.0) (not $x58))) (= (not (< a$ 0.0)) (not (not $x58)))))) +(let ((@x66 (trans @x62 (rewrite (= (not (not $x58)) $x58)) (= (not (< a$ 0.0)) $x58)))) +(let ((@x67 (mp (asserted (not (< a$ 0.0))) @x66 $x58))) +((_ th-lemma arith farkas 7 3/2 1) @x67 @x52 @x40 false))))))))))))))))) + 7d3773a9d63ce2ada82ac001b84291cdc85d7ab8 159 0 unsat ((set-logic AUFLIA) @@ -3538,43 +3538,10 @@ (let ((@x125 (mp (mp @x110 (quant-intro @x115 (= $x107 $x116)) $x116) (quant-intro (rewrite (= $x113 $x104)) (= $x116 $x122)) $x122))) (mp (mp @x125 @x156 $x152) @x180 false)))))))))))))))))))))))))))))))))))))))))))))) -79a22a7943e8703e97ab2cddee03d311bc7ae2a6 36 0 -unsat -((set-logic AUFLIA) -(proof -(let (($x35 (forall ((?v0 Int) )(let ((?x32 (* 2 a$))) -(let ((?x31 (* 2 ?v0))) -(let (($x33 (< ?x31 ?x32))) -(let (($x29 (< ?v0 a$))) -(=> $x29 $x33)))))) -)) -(let (($x36 (not $x35))) -(let (($x42 (forall ((?v0 Int) )(let ((?x32 (* 2 a$))) -(let ((?x31 (* 2 ?v0))) -(let (($x33 (< ?x31 ?x32))) -(let (($x29 (< ?v0 a$))) -(let (($x38 (not $x29))) -(or $x38 $x33))))))) -)) -(let (($x45 (not $x42))) -(let (($x71 (forall ((?v0 Int) )true) -)) -(let ((?x32 (* 2 a$))) -(let ((?x31 (* 2 ?0))) -(let (($x33 (< ?x31 ?x32))) -(let (($x29 (< ?0 a$))) -(let (($x38 (not $x29))) -(let (($x39 (or $x38 $x33))) -(let (($x50 (>= (+ ?0 (* (- 1) a$)) 0))) -(let (($x49 (not $x50))) -(let ((@x61 (trans (monotonicity (rewrite (= $x29 $x49)) (= $x38 (not $x49))) (rewrite (= (not $x49) $x50)) (= $x38 $x50)))) -(let ((@x66 (monotonicity @x61 (rewrite (= $x33 $x49)) (= $x39 (or $x50 $x49))))) -(let ((@x73 (quant-intro (trans @x66 (rewrite (= (or $x50 $x49) true)) (= $x39 true)) (= $x42 $x71)))) -(let ((@x80 (monotonicity (trans @x73 (elim-unused (= $x71 true)) (= $x42 true)) (= $x45 (not true))))) -(let ((@x84 (trans @x80 (rewrite (= (not true) false)) (= $x45 false)))) -(let ((@x47 (monotonicity (quant-intro (rewrite (= (=> $x29 $x33) $x39)) (= $x35 $x42)) (= $x36 $x45)))) -(mp (asserted $x36) (trans @x47 @x84 (= $x36 false)) false)))))))))))))))))))))) - +68af267a155ec93a64652d04b7ee09ecad3d48b9 3 0 +(error "line 5 column 91: invalid function application, arguments missing") +sat +(error "line 7 column 10: proof is not available") ae4f4fb9c10608b8e3b893cc6c99e3ec5d13a86c 24 0 unsat ((set-logic AUFLIA) @@ -3944,22 +3911,7 @@ (let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false)))) (mp (asserted $x33) @x53 false))))))))))) -8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0 -unsat -((set-logic AUFLIA) -(proof -(let (($x29 (forall ((?v0 A$) )(g$ ?v0)) -)) -(let (($x30 (ite $x29 true false))) -(let (($x31 (f$ $x30))) -(let (($x32 (=> $x31 true))) -(let (($x33 (not $x32))) -(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true))))) -(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true)))) -(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false)))) -(mp (asserted $x33) @x53 false))))))))))) - -b221de9d8dbe279344ac85e2ada07f5722636ce5 46 0 +feaa6ef662dd489cf55f86209489c2992ff08d28 46 0 unsat ((set-logic AUFLIA) (proof @@ -4006,7 +3958,34 @@ (let ((@x478 (mp ((_ quant-inst 3 42) (or (not $x52) $x171)) (trans (monotonicity @x131 $x137) (rewrite (= $x134 $x134)) $x137) $x134))) (unit-resolution (unit-resolution @x478 @x78 $x168) (mp @x77 @x472 (not $x168)) false))))))))))))))))))))))))))))))))))) -5d3ccbcf168a634cad3952ad8f6d2798329d6a77 75 0 +8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0 +unsat +((set-logic AUFLIA) +(proof +(let (($x29 (forall ((?v0 A$) )(g$ ?v0)) +)) +(let (($x30 (ite $x29 true false))) +(let (($x31 (f$ $x30))) +(let (($x32 (=> $x31 true))) +(let (($x33 (not $x32))) +(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true))))) +(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true)))) +(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false)))) +(mp (asserted $x33) @x53 false))))))))))) + +40c61a0200976d6203302a7343af5b7ad1e6ce36 11 0 +unsat +((set-logic AUFLIA) +(proof +(let (($x29 (forall ((?v0 A$) )(p$ ?v0)) +)) +(let (($x30 (not $x29))) +(let (($x31 (or $x29 $x30))) +(let (($x32 (not $x31))) +(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false)))) +(mp (asserted $x32) @x42 false)))))))) + +9cdd1051dbf4e0648f71536fbc74bbab8e0e744e 75 0 unsat ((set-logic AUFLIA) (proof @@ -4082,18 +4061,6 @@ (let ((@x82 (asserted $x81))) (unit-resolution @x82 @x466 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -40c61a0200976d6203302a7343af5b7ad1e6ce36 11 0 -unsat -((set-logic AUFLIA) -(proof -(let (($x29 (forall ((?v0 A$) )(p$ ?v0)) -)) -(let (($x30 (not $x29))) -(let (($x31 (or $x29 $x30))) -(let (($x32 (not $x31))) -(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false)))) -(mp (asserted $x32) @x42 false)))))))) - f17a5e4d5f1a5a93fbc847f858c7c845c29d8349 109 0 unsat ((set-logic AUFLIA) @@ -4204,7 +4171,7 @@ (let ((@x81 (asserted $x80))) (unit-resolution @x81 (trans @x397 ((_ th-lemma arith eq-propagate 1 1 -4 -4) @x410 @x422 @x428 @x438 (= ?x490 6)) $x79) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -16cd6b3ca7edac6486d6ca7a72e97f4ad1c07e37 336 0 +8c0c900f4d4a92edc7d6113704948dc9280df015 336 0 unsat ((set-logic ) (proof @@ -4541,7 +4508,7 @@ (let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281))) (unit-resolution @x472 @x889 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -d277a40ca34ecc409672601e981711fef2d0064f 64 0 +db184ed715734759b60f9bdc99290a92283563f5 64 0 unsat ((set-logic AUFLIA) (proof diff -r 1da9b8045026 -r db5a718e8c09 src/HOL/SMT_Examples/SMT_Examples.thy --- a/src/HOL/SMT_Examples/SMT_Examples.thy Mon Nov 24 12:35:13 2014 +0100 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy Mon Nov 24 12:35:13 2014 +0100 @@ -354,9 +354,6 @@ lemma "\x::int. \x y. 0 < x \ 0 < y \ (0::int) < x + y" by smt lemma "\u::int. \(x::int) y::real. 0 < x \ 0 < y \ -1 < x" by smt lemma "\x::int. (\y. y \ x \ y > 0) \ x > 0" by smt -lemma "\x::int. - SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat x) SMT.Symb_Nil) SMT.Symb_Nil) - (x < a \ 2 * x < 2 * a)" by smt lemma "\(a::int) b::int. 0 < b \ b < 1" by smt diff -r 1da9b8045026 -r db5a718e8c09 src/HOL/SMT_Examples/SMT_Word_Examples.certs --- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs Mon Nov 24 12:35:13 2014 +0100 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs Mon Nov 24 12:35:13 2014 +0100 @@ -1,11 +1,3 @@ -aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0 -unsat -((set-logic ) -(proof -(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true))))) -(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false)))) -(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false))))) - 8e6fd56de8adc20c29f4bdb8c2c55e63988185a8 8 0 unsat ((set-logic ) @@ -15,6 +7,14 @@ (let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false)))) (mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false)))))) +aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0 +unsat +((set-logic ) +(proof +(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true))))) +(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false)))) +(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false))))) + a14afea8a52a1586ff44eff03b88f1717144d17a 7 0 unsat ((set-logic ) @@ -43,14 +43,6 @@ (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false)))) (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false))))))) -6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0 -unsat -((set-logic ) -(proof -(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) -(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) -(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false))))) - 45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0 unsat ((set-logic ) @@ -61,6 +53,14 @@ (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false)))) (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false))))))) +6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0 +unsat +((set-logic ) +(proof +(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) +(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) +(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false))))) + 00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0 unsat ((set-logic ) @@ -73,16 +73,6 @@ (let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false)))) (mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false))))))))) -d150015a66b6757a72346710966844993c0f3c27 9 0 -unsat -((set-logic ) -(proof -(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32)))))) -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true)))) -(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true))))) -(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false)))) -(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false))))))) - b4600e6d14c88b633ac7bcc5b2e24af8539b0218 18 0 unsat ((set-logic ) @@ -122,15 +112,15 @@ (let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false)))) (mp (asserted $x38) @x67 false))))))))))))))))) -d7cc0827eb340c29b0f489145022e4b3e3610818 9 0 +d150015a66b6757a72346710966844993c0f3c27 9 0 unsat ((set-logic ) (proof -(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8)))))) -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) -(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) -(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) -(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false))))))) +(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32)))))) +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true)))) +(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true))))) +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false)))) +(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false))))))) 200e29aa9f19844d244c5c9755155eb956c5cf7c 9 0 unsat @@ -142,6 +132,16 @@ (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false)))) (mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false))))))) +d7cc0827eb340c29b0f489145022e4b3e3610818 9 0 +unsat +((set-logic ) +(proof +(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8)))))) +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) +(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) +(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false))))))) + 3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0 unsat ((set-logic ) @@ -151,6 +151,16 @@ (let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false)))) (mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false)))))) +14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0 +unsat +((set-logic ) +(proof +(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) +(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) +(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false))))))) + 880bee16a8f6469b14122277b92e87533ef6a071 9 0 unsat ((set-logic ) @@ -161,16 +171,6 @@ (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false)))) (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false))))))) -14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0 -unsat -((set-logic ) -(proof -(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) -(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) -(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) -(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false))))))) - b48f55cefc567df166d8e9967c53372c30620183 8 0 unsat ((set-logic ) diff -r 1da9b8045026 -r db5a718e8c09 src/HOL/SMT_Examples/VCC_Max.certs --- a/src/HOL/SMT_Examples/VCC_Max.certs Mon Nov 24 12:35:13 2014 +0100 +++ b/src/HOL/SMT_Examples/VCC_Max.certs Mon Nov 24 12:35:13 2014 +0100 @@ -1,4 +1,4 @@ -05a761f33f246f0fee720bec6f015ca5aba01c4d 2972 0 +8ec9d30fc9fdbc0ea292e0fdf148a6230c16dbca 2972 0 unsat ((set-logic ) (declare-fun ?v0!14 () Int)