--- 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 <null>)
(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
--- 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 "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt
lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt
lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
-lemma "\<forall>x::int.
- SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat x) SMT.Symb_Nil) SMT.Symb_Nil)
- (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt
--- 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 <null>)
-(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 <null>)
@@ -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 <null>)
+(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 <null>)
@@ -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 <null>)
-(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 <null>)
@@ -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 <null>)
+(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 <null>)
@@ -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 <null>)
-(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 <null>)
@@ -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 <null>)
(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 <null>)
+(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 <null>)
@@ -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 <null>)
+(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 <null>)
@@ -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 <null>)
-(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 <null>)
--- 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 <null>)
(declare-fun ?v0!14 () Int)