# HG changeset patch # User fleury # Date 1406721793 -7200 # Node ID caadd484dec69e6a83a77416544d0b37411c01bf # Parent 323a57d7455ce222a01365d5cbdffa69f5d4c187 Changing ~ into - for unuary minus (not supported by veriT) diff -r 323a57d7455c -r caadd484dec6 src/HOL/SMT_Examples/SMT_Examples.certs2 --- a/src/HOL/SMT_Examples/SMT_Examples.certs2 Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs2 Wed Jul 30 14:03:13 2014 +0200 @@ -1,10 +1,3 @@ -3aa17d1c77bc1a92bca05df291d11d81c645a931 6 0 -unsat -((set-logic AUFLIA) -(proof -(let ((@x30 (rewrite (= (not true) false)))) -(mp (asserted (not true)) @x30 false)))) - 572677daa32981bf8212986300f1362edf42a0c1 7 0 unsat ((set-logic AUFLIA) @@ -13,6 +6,13 @@ (let ((@x40 (trans @x36 (rewrite (= (not true) false)) (= (not (or p$ (not p$))) false)))) (mp (asserted (not (or p$ (not p$)))) @x40 false))))) +3aa17d1c77bc1a92bca05df291d11d81c645a931 6 0 +unsat +((set-logic AUFLIA) +(proof +(let ((@x30 (rewrite (= (not true) false)))) +(mp (asserted (not true)) @x30 false)))) + dfd95b23f80baacb2acdc442487bd8121f072035 9 0 unsat ((set-logic AUFLIA) @@ -1033,7 +1033,7 @@ (let ((@x59 (trans @x55 (rewrite (= (not true) false)) (= (not (< 5 (ite (<= 3 8) 8 3))) false)))) (mp (asserted (not (< 5 (ite (<= 3 8) 8 3)))) @x59 false))))))))) -2d63144daf211d89368e355b9b23a3b5118b7ba9 88 0 +6b0b089fbe179e8a27509c818f9a5e6847ac6bf2 88 0 unsat ((set-logic AUFLIRA) (proof @@ -1207,7 +1207,7 @@ (let ((@x67 (mp (asserted (not (< a$ 0.0))) @x66 $x58))) ((_ th-lemma arith farkas 7 3/2 1) @x67 @x52 @x40 false))))))))))))))))) -b9f61649fae66ac195bf2593181f9d76c958bfe2 22 0 +3a6df2b095b936aac9a1d533e306f2d31b4fb44e 22 0 unsat ((set-logic AUFLIA) (proof @@ -1390,7 +1390,7 @@ (let ((@x433 (mp (not-or-elim @x205 (not $x57)) @x432 $x422))) (unit-resolution @x433 @x488 (mp @x478 @x480 $x44) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -fbc59441c65d9a844da44405d06d138b55c5d187 933 0 +32286f9c5e71eb2b15c18f86f04c80931e2e307b 933 0 unsat ((set-logic AUFLIA) (proof @@ -2345,7 +2345,7 @@ (let ((@x62 (monotonicity @x59 (= $x36 (not $x43))))) (mp (asserted $x36) (trans @x62 @x71 (= $x36 false)) false)))))))))))))))))) -d2037888c28cf52f7a45f66288246169de6f14ad 113 0 +faae12ee7efe4347f92e42776a0e0e57a624319c 113 0 unsat ((set-logic ) (proof @@ -2459,7 +2459,7 @@ (let ((@x74 (mp (asserted $x36) @x73 $x67))) ((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -29e336c1b1dbb5e85401e6a2954560661ff3cadc 112 0 +57f344c9e787868c98d1e622f158c445c1899c96 112 0 unsat ((set-logic ) (proof @@ -2572,7 +2572,7 @@ (let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63))) ((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -5bcedd8db3cccf5f1df2ef7ad1ca5e39c817a6f4 32 0 +3938db798ebafb55191dcdaf83a8615d1d59c0c3 32 0 unsat ((set-logic ) (proof @@ -2605,7 +2605,7 @@ (let ((@x117 (unit-resolution ((_ th-lemma arith assign-bounds 1) (or $x102 (not $x100))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x95) $x100)) @x98 $x100) $x102))) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x28 (not $x101) (not $x102))) @x117 @x110 @x30 false)))))))))))))))))))))))))))))) -97186805a3315ef9a1cc4847a2e19a6d09c77915 236 0 +353c8b65ed1b98772a89ffdae52f1cfae628dd6a 236 0 unsat ((set-logic ) (proof @@ -3224,7 +3224,7 @@ (let ((@x66 (mp~ (mp (asserted $x33) @x60 $x56) (nnf-pos (refl (~ $x53 $x53)) (~ $x56 $x56)) $x56))) (unit-resolution @x66 @x464 false))))))))))))))))))))))))) -a8cb4a130675f119ab8ba11cbe3a15041f18d2c6 62 0 +a02ae6c9688537bbe4c3be0d3dcebbc703417864 62 0 unsat ((set-logic AUFLIA) (declare-fun ?v0!1 () Int) @@ -3287,7 +3287,7 @@ (let ((@x515 (unit-resolution (def-axiom (or z3name!0 $x220)) (unit-resolution @x131 @x238 $x88) $x220))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x220) (>= ?x96 3))) @x515 @x245 false)))))))))))))))))))))))))))))))))))))))))))))))))))))) -9e0e67e5bd5078ab683d440f1a73c518a403be1b 39 0 +9853592ad3514c1450e40271884a9f21f57ff85b 39 0 unsat ((set-logic AUFLIA) (proof @@ -3380,7 +3380,7 @@ (let ((@x117 (and-elim (not-or-elim @x112 (and $x100 $x102)) $x102))) ((_ th-lemma arith farkas 1 1 1) @x117 @x116 @x118 false))))))))))))))))))))))))))))))))))) -0d380fa4e68ab250e8351813b95695943794f02d 46 0 +9201a8009730b821ad6a3a2b64598e50ab5748ca 46 0 unsat ((set-logic AUFLIRA) (declare-fun ?v1!1 () Int) @@ -3600,6 +3600,33 @@ (let ((@x73 (not-or-elim @x70 $x62))) (unit-resolution (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x65 (not $x62))) @x73 $x65) @x74 false)))))))))))))))))) +d98ad8f668dead6f610669a52351ea0176a811b0 26 0 +unsat +((set-logic ) +(proof +(let (($x58 (<= b$ 0))) +(let (($x62 (or (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0)))) (not $x58)))) +(let (($x65 (not $x62))) +(let (($x35 (not (=> (and (< 0 a$) (< 0 (* a$ b$))) (< 0 b$))))) +(let (($x33 (< 0 b$))) +(let (($x38 (or (not (and (< 0 a$) (< 0 (* a$ b$)))) $x33))) +(let (($x56 (= (not (and (< 0 a$) (< 0 (* a$ b$)))) (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0))))))) +(let ((?x30 (* a$ b$))) +(let (($x48 (<= ?x30 0))) +(let (($x49 (not $x48))) +(let (($x44 (<= a$ 0))) +(let (($x45 (not $x44))) +(let (($x52 (and $x45 $x49))) +(let (($x32 (and (< 0 a$) (< 0 ?x30)))) +(let ((@x54 (monotonicity (rewrite (= (< 0 a$) $x45)) (rewrite (= (< 0 ?x30) $x49)) (= $x32 $x52)))) +(let ((@x64 (monotonicity (monotonicity @x54 $x56) (rewrite (= $x33 (not $x58))) (= $x38 $x62)))) +(let ((@x43 (monotonicity (rewrite (= (=> $x32 $x33) $x38)) (= $x35 (not $x38))))) +(let ((@x69 (trans @x43 (monotonicity @x64 (= (not $x38) $x65)) (= $x35 $x65)))) +(let ((@x74 (not-or-elim (mp (asserted $x35) @x69 $x65) $x58))) +(let ((@x72 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x45))) +(let ((@x73 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x49))) +((_ th-lemma arith farkas 1 1 1) @x73 @x72 @x74 false)))))))))))))))))))))))) + 271390ea915947de195c2202e30f90bb84689d60 26 0 unsat ((set-logic ) @@ -3627,33 +3654,6 @@ (let ((@x92 (trans @x88 (rewrite (= (not true) false)) (= $x39 false)))) (mp (asserted $x39) @x92 false)))))))))))))))))))))))) -d98ad8f668dead6f610669a52351ea0176a811b0 26 0 -unsat -((set-logic ) -(proof -(let (($x58 (<= b$ 0))) -(let (($x62 (or (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0)))) (not $x58)))) -(let (($x65 (not $x62))) -(let (($x35 (not (=> (and (< 0 a$) (< 0 (* a$ b$))) (< 0 b$))))) -(let (($x33 (< 0 b$))) -(let (($x38 (or (not (and (< 0 a$) (< 0 (* a$ b$)))) $x33))) -(let (($x56 (= (not (and (< 0 a$) (< 0 (* a$ b$)))) (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0))))))) -(let ((?x30 (* a$ b$))) -(let (($x48 (<= ?x30 0))) -(let (($x49 (not $x48))) -(let (($x44 (<= a$ 0))) -(let (($x45 (not $x44))) -(let (($x52 (and $x45 $x49))) -(let (($x32 (and (< 0 a$) (< 0 ?x30)))) -(let ((@x54 (monotonicity (rewrite (= (< 0 a$) $x45)) (rewrite (= (< 0 ?x30) $x49)) (= $x32 $x52)))) -(let ((@x64 (monotonicity (monotonicity @x54 $x56) (rewrite (= $x33 (not $x58))) (= $x38 $x62)))) -(let ((@x43 (monotonicity (rewrite (= (=> $x32 $x33) $x38)) (= $x35 (not $x38))))) -(let ((@x69 (trans @x43 (monotonicity @x64 (= (not $x38) $x65)) (= $x35 $x65)))) -(let ((@x74 (not-or-elim (mp (asserted $x35) @x69 $x65) $x58))) -(let ((@x72 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x45))) -(let ((@x73 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x49))) -((_ th-lemma arith farkas 1 1 1) @x73 @x72 @x74 false)))))))))))))))))))))))) - b216c79478e44396acca3654b76845499fc18a04 23 0 unsat ((set-logic ) @@ -3944,6 +3944,21 @@ (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 unsat ((set-logic AUFLIA) @@ -3991,21 +4006,6 @@ (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))))))))))))))))))))))))))))))))))) -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))))))))))) - 5d3ccbcf168a634cad3952ad8f6d2798329d6a77 75 0 unsat ((set-logic AUFLIA) @@ -4204,7 +4204,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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -fa62bf7228a50eb8c663092f87f9af7c25feaffe 336 0 +640bb6103260f74026864b86c2301c00ea737ff0 336 0 unsat ((set-logic ) (proof diff -r 323a57d7455c -r caadd484dec6 src/HOL/SMT_Examples/SMT_Word_Examples.certs2 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs2 Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs2 Wed Jul 30 14:03:13 2014 +0200 @@ -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 ) @@ -142,6 +142,15 @@ (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 ) +(proof +(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) +(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) +(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 ) @@ -152,14 +161,15 @@ (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))))))) -3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0 +880bee16a8f6469b14122277b92e87533ef6a071 9 0 unsat ((set-logic ) (proof -(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) -(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) -(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)))))) +(let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) +(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) +(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))))))) 8d29c9b5ef712a3d9d2db87383c9c25c0b553e01 8 0 unsat @@ -170,16 +180,6 @@ (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)))) (mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false)))))) -880bee16a8f6469b14122277b92e87533ef6a071 9 0 -unsat -((set-logic ) -(proof -(let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) -(let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) -(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) -(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))))))) - 446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 9 0 unsat ((set-logic ) @@ -240,6 +240,16 @@ (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false)))) (mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false))))))) +33a52e620069e1ecebbc00aa6b0099170558c111 9 0 +unsat +((set-logic ) +(proof +(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4)))))) +(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true)))) +(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true))))) +(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false)))) +(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false))))))) + 5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0 unsat ((set-logic ) @@ -258,46 +268,6 @@ (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))) (unit-resolution @x55 @x63 false))))))))))))))) -33a52e620069e1ecebbc00aa6b0099170558c111 9 0 -unsat -((set-logic ) -(proof -(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4)))))) -(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true)))) -(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true))))) -(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false)))) -(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false))))))) - -115ab22c9945d493b971e69a38d9e608c5b40a71 29 0 -unsat -((set-logic ) -(proof -(let ((?x28 (bv2int$ (_ bv0 2)))) -(let (($x183 (<= ?x28 0))) -(let (($x184 (not $x183))) -(let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0))) -(let (($x53 (<= ?x47 0))) -(not $x53))) :pattern ( (bv2int$ ?v0) ))) -)) -(let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) -(let (($x53 (<= ?x47 0))) -(not $x53)))) -)) -(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) -(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) -(let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) -(< 0 ?x47))) -)) -(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0)))))) -(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57))) -(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175))) -(let (($x187 (not $x175))) -(let (($x188 (or $x187 $x184))) -(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188))) -(let (($x29 (= ?x28 0))) -(let ((@x30 (asserted $x29))) -(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false))))))))))))))))))) - 1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0 unsat ((set-logic ) @@ -350,6 +320,36 @@ (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))) (unit-resolution @x314 @x322 false))))))))))))))))))))))))))))))))))))))))))))))))) +115ab22c9945d493b971e69a38d9e608c5b40a71 29 0 +unsat +((set-logic ) +(proof +(let ((?x28 (bv2int$ (_ bv0 2)))) +(let (($x183 (<= ?x28 0))) +(let (($x184 (not $x183))) +(let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0))) +(let (($x53 (<= ?x47 0))) +(not $x53))) :pattern ( (bv2int$ ?v0) ))) +)) +(let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) +(let (($x53 (<= ?x47 0))) +(not $x53)))) +)) +(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) +(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) +(let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) +(< 0 ?x47))) +)) +(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0)))))) +(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57))) +(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175))) +(let (($x187 (not $x175))) +(let (($x188 (or $x187 $x184))) +(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188))) +(let (($x29 (= ?x28 0))) +(let ((@x30 (asserted $x29))) +(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false))))))))))))))))))) + d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0 unsat ((set-logic ) diff -r 323a57d7455c -r caadd484dec6 src/HOL/Tools/SMT2/smt2_real.ML --- a/src/HOL/Tools/SMT2/smt2_real.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_real.ML Wed Jul 30 14:03:13 2014 +0200 @@ -36,7 +36,7 @@ fold (SMT2_Builtin.add_builtin_fun' SMTLIB2_Interface.smtlib2C) [ (@{const less (real)}, "<"), (@{const less_eq (real)}, "<="), - (@{const uminus (real)}, "~"), + (@{const uminus (real)}, "-"), (@{const plus (real)}, "+"), (@{const minus (real)}, "-") ] #> SMT2_Builtin.add_builtin_fun SMTLIB2_Interface.smtlib2C diff -r 323a57d7455c -r caadd484dec6 src/HOL/Tools/SMT2/smtlib2_interface.ML --- a/src/HOL/Tools/SMT2/smtlib2_interface.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML Wed Jul 30 14:03:13 2014 +0200 @@ -49,7 +49,7 @@ (@{const If ('a)}, "ite"), (@{const less (int)}, "<"), (@{const less_eq (int)}, "<="), - (@{const uminus (int)}, "~"), + (@{const uminus (int)}, "-"), (@{const plus (int)}, "+"), (@{const minus (int)}, "-")] #> SMT2_Builtin.add_builtin_fun smtlib2C