# HG changeset patch # User boehmes # Date 1269644307 -3600 # Node ID bd4e0d68c56d0b5f8dd31affe9b58af5ef439632 # Parent 344afccb09d114079df974bc074773013a4c42eb updated SMT certificates diff -r 344afccb09d1 -r bd4e0d68c56d src/HOL/Boogie/Examples/Boogie_Dijkstra.certs --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Fri Mar 26 23:57:35 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Fri Mar 26 23:58:27 2010 +0100 @@ -1,4 +1,4 @@ -6164a2366a9e57e212b8ac4aa01e3c8bcc1ea8e0 6542 0 +d29d9bae6b4b919e45b23de87975f8734cce2039 6542 0 #2 := false decl up_6 :: (-> T4 T2 bool) decl ?x47!7 :: (-> T2 T2) diff -r 344afccb09d1 -r bd4e0d68c56d src/HOL/Boogie/Examples/Boogie_Max.certs --- a/src/HOL/Boogie/Examples/Boogie_Max.certs Fri Mar 26 23:57:35 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Max.certs Fri Mar 26 23:58:27 2010 +0100 @@ -1,4 +1,4 @@ -cdfef9f27f2a4ba9648f86890c8563d0a1cfe888 2224 0 +eafecd70b5ba5010589b5ae443c033b4aa8eb332 2224 0 #2 := false #4 := 0::int decl uf_3 :: (-> int int) diff -r 344afccb09d1 -r bd4e0d68c56d src/HOL/Boogie/Examples/VCC_Max.certs --- a/src/HOL/Boogie/Examples/VCC_Max.certs Fri Mar 26 23:57:35 2010 +0100 +++ b/src/HOL/Boogie/Examples/VCC_Max.certs Fri Mar 26 23:58:27 2010 +0100 @@ -1,4 +1,4 @@ -b95bf7adc1e2b959cf13db317b64554768249b2e 7790 0 +ecd63e557c7e66d192e7c9b7445f98b44f79ca34 7790 0 #2 := false decl uf_110 :: (-> T4 T5 int) decl uf_66 :: (-> T5 int T3 T5) diff -r 344afccb09d1 -r bd4e0d68c56d src/HOL/Multivariate_Analysis/Integration.cert --- a/src/HOL/Multivariate_Analysis/Integration.cert Fri Mar 26 23:57:35 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.cert Fri Mar 26 23:58:27 2010 +0100 @@ -1,4 +1,4 @@ -534d3afbd3505abffa6b03e3986bfa7aa3cff358 428 0 +9d0325fd923020e9d1f3e7c851ac5a92d68bdbdf 428 0 #2 := false decl uf_10 :: T1 #38 := uf_10 @@ -427,7 +427,7 @@ #674 := [lemma #673]: #571 [unit-resolution #674 #690]: false unsat -985f86fd1ea01264c02b8076ffd658677bd4d29a 419 0 +c87f23eea66c69622dc5ab167ea6f34f69f5b963 419 0 #2 := false #194 := 0::real decl uf_4 :: (-> T2 T3 real) @@ -847,7 +847,7 @@ #224 := [and-elim #222]: #214 [th-lemma #224 #275 #689]: false unsat -00b949278548f13329cf92f11a0ad2161fa40793 907 0 +1596317f793892bf21292b98f5b9358a7fbbbc34 907 0 #2 := false #299 := 0::real decl uf_1 :: (-> T3 T2 real) @@ -1755,7 +1755,7 @@ #1366 := [unit-resolution #1233 #1365]: #1231 [th-lemma #1366 #1364 #1362]: false unsat -f5cf3017773c1cf700f533cb220ba6c9eb22de56 211 0 +697101e22cd936070cda4e34ef646648761a3ec5 211 0 #2 := false #33 := 0::real decl uf_11 :: (-> T5 T6 real) @@ -1967,7 +1967,7 @@ #328 := [unit-resolution #319 #327]: #300 [th-lemma #326 #334 #195 #328 #187 #138]: false unsat -ad41c2d9b185dd9b4fd0abefcdc55357d2105ed8 285 0 +76dd2264ac7b34ef64af3aea7f49f78e51b20a36 285 0 #2 := false #7 := 0::real decl uf_4 :: real @@ -2253,7 +2253,7 @@ #286 := [lemma #284]: #285 [unit-resolution #286 #308 #305]: false unsat -076d8565ad4c4370b16a3b0c139e8c8e8fb58224 97 0 +5bc83521693fc90ddbd62a1d655c9b76740f7f5c 97 0 #2 := false #18 := 0::real decl uf_1 :: (-> T2 T1 real) @@ -2351,7 +2351,7 @@ #173 := [mp #167 #172]: #165 [unit-resolution #173 #147 #76]: false unsat -8e6ea05b53a9ffb5a6dec689eb004bdb0c2a755b 57 0 +537f6487ce8905f62d380a496ea77f3492821720 57 0 #2 := false #4 := 0::real decl uf_1 :: (-> T2 real) @@ -2409,7 +2409,7 @@ #269 := [quant-inst]: #268 [unit-resolution #269 #247 #274]: false unsat -d278c38176edc1fb6492d54817f0a9092db653e6 91 0 +6ed731a5c059cb83dd6a40492311dd9bf8e4de9b 91 0 #2 := false #38 := 0::real decl uf_1 :: (-> T1 T2 real) @@ -2501,7 +2501,7 @@ #153 := [mp #147 #152]: #145 [unit-resolution #153 #129 #160]: false unsat -38b5e95092f91070fab780891ebf7b83d5f95757 222 0 +283acece9403e0ed1dff5dca04d9b1e77248a71c 222 0 #2 := false #4 := 0::real decl uf_2 :: (-> T2 T1 real) @@ -2724,7 +2724,7 @@ #308 := [th-lemma]: #307 [unit-resolution #308 #305 #290]: false unsat -4968b0a0840255d92fbecd59ed4dac302603b2bd 248 0 +c140056bfbcb9e3878073e8d474395da7df06aaf 248 0 #2 := false #4 := 0::real decl uf_2 :: (-> T2 T1 real) @@ -2973,7 +2973,94 @@ #380 := [th-lemma]: #379 [unit-resolution #380 #377 #363]: false unsat -a3b02dd75d8b2261f1b7ef7215268d84fd25e972 149 0 +9df215500c4e556185e187283e11a68edbd664b5 86 0 +#2 := false +#37 := 0::real +decl uf_2 :: (-> T2 T1 real) +decl uf_4 :: T1 +#12 := uf_4 +decl uf_3 :: T2 +#5 := uf_3 +#13 := (uf_2 uf_3 uf_4) +#34 := -1::real +#140 := (* -1::real #13) +decl uf_1 :: real +#4 := uf_1 +#141 := (+ uf_1 #140) +#143 := (>= #141 0::real) +#6 := (:var 0 T1) +#7 := (uf_2 uf_3 #6) +#127 := (pattern #7) +#35 := (* -1::real #7) +#36 := (+ uf_1 #35) +#47 := (>= #36 0::real) +#134 := (forall (vars (?x2 T1)) (:pat #127) #47) +#49 := (forall (vars (?x2 T1)) #47) +#137 := (iff #49 #134) +#135 := (iff #47 #47) +#136 := [refl]: #135 +#138 := [quant-intro #136]: #137 +#67 := (~ #49 #49) +#58 := (~ #47 #47) +#66 := [refl]: #58 +#68 := [nnf-pos #66]: #67 +#10 := (<= #7 uf_1) +#11 := (forall (vars (?x2 T1)) #10) +#50 := (iff #11 #49) +#46 := (iff #10 #47) +#48 := [rewrite]: #46 +#51 := [quant-intro #48]: #50 +#32 := [asserted]: #11 +#52 := [mp #32 #51]: #49 +#69 := [mp~ #52 #68]: #49 +#139 := [mp #69 #138]: #134 +#149 := (not #134) +#150 := (or #149 #143) +#151 := [quant-inst]: #150 +#144 := [unit-resolution #151 #139]: #143 +#142 := (<= #141 0::real) +#38 := (<= #36 0::real) +#128 := (forall (vars (?x1 T1)) (:pat #127) #38) +#41 := (forall (vars (?x1 T1)) #38) +#131 := (iff #41 #128) +#129 := (iff #38 #38) +#130 := [refl]: #129 +#132 := [quant-intro #130]: #131 +#62 := (~ #41 #41) +#64 := (~ #38 #38) +#65 := [refl]: #64 +#63 := [nnf-pos #65]: #62 +#8 := (<= uf_1 #7) +#9 := (forall (vars (?x1 T1)) #8) +#42 := (iff #9 #41) +#39 := (iff #8 #38) +#40 := [rewrite]: #39 +#43 := [quant-intro #40]: #42 +#31 := [asserted]: #9 +#44 := [mp #31 #43]: #41 +#61 := [mp~ #44 #63]: #41 +#133 := [mp #61 #132]: #128 +#145 := (not #128) +#146 := (or #145 #142) +#147 := [quant-inst]: #146 +#148 := [unit-resolution #147 #133]: #142 +#45 := (= uf_1 #13) +#55 := (not #45) +#14 := (= #13 uf_1) +#15 := (not #14) +#56 := (iff #15 #55) +#53 := (iff #14 #45) +#54 := [rewrite]: #53 +#57 := [monotonicity #54]: #56 +#33 := [asserted]: #15 +#60 := [mp #33 #57]: #55 +#153 := (not #143) +#152 := (not #142) +#154 := (or #45 #152 #153) +#155 := [th-lemma]: #154 +[unit-resolution #155 #60 #148 #144]: false +unsat +7e78f7c132b9e8e998decefbcdf818aa16be5cc1 149 0 #2 := false #19 := 0::real decl uf_1 :: (-> T1 T2 real) @@ -3123,90 +3210,3 @@ #228 := [unit-resolution #200 #220]: #173 [th-lemma #228 #227 #211]: false unsat -06d4133eb0950a5f12d22480aa2707e31af2b064 86 0 -#2 := false -#37 := 0::real -decl uf_2 :: (-> T2 T1 real) -decl uf_4 :: T1 -#12 := uf_4 -decl uf_3 :: T2 -#5 := uf_3 -#13 := (uf_2 uf_3 uf_4) -#34 := -1::real -#140 := (* -1::real #13) -decl uf_1 :: real -#4 := uf_1 -#141 := (+ uf_1 #140) -#143 := (>= #141 0::real) -#6 := (:var 0 T1) -#7 := (uf_2 uf_3 #6) -#127 := (pattern #7) -#35 := (* -1::real #7) -#36 := (+ uf_1 #35) -#47 := (>= #36 0::real) -#134 := (forall (vars (?x2 T1)) (:pat #127) #47) -#49 := (forall (vars (?x2 T1)) #47) -#137 := (iff #49 #134) -#135 := (iff #47 #47) -#136 := [refl]: #135 -#138 := [quant-intro #136]: #137 -#67 := (~ #49 #49) -#58 := (~ #47 #47) -#66 := [refl]: #58 -#68 := [nnf-pos #66]: #67 -#10 := (<= #7 uf_1) -#11 := (forall (vars (?x2 T1)) #10) -#50 := (iff #11 #49) -#46 := (iff #10 #47) -#48 := [rewrite]: #46 -#51 := [quant-intro #48]: #50 -#32 := [asserted]: #11 -#52 := [mp #32 #51]: #49 -#69 := [mp~ #52 #68]: #49 -#139 := [mp #69 #138]: #134 -#149 := (not #134) -#150 := (or #149 #143) -#151 := [quant-inst]: #150 -#144 := [unit-resolution #151 #139]: #143 -#142 := (<= #141 0::real) -#38 := (<= #36 0::real) -#128 := (forall (vars (?x1 T1)) (:pat #127) #38) -#41 := (forall (vars (?x1 T1)) #38) -#131 := (iff #41 #128) -#129 := (iff #38 #38) -#130 := [refl]: #129 -#132 := [quant-intro #130]: #131 -#62 := (~ #41 #41) -#64 := (~ #38 #38) -#65 := [refl]: #64 -#63 := [nnf-pos #65]: #62 -#8 := (<= uf_1 #7) -#9 := (forall (vars (?x1 T1)) #8) -#42 := (iff #9 #41) -#39 := (iff #8 #38) -#40 := [rewrite]: #39 -#43 := [quant-intro #40]: #42 -#31 := [asserted]: #9 -#44 := [mp #31 #43]: #41 -#61 := [mp~ #44 #63]: #41 -#133 := [mp #61 #132]: #128 -#145 := (not #128) -#146 := (or #145 #142) -#147 := [quant-inst]: #146 -#148 := [unit-resolution #147 #133]: #142 -#45 := (= uf_1 #13) -#55 := (not #45) -#14 := (= #13 uf_1) -#15 := (not #14) -#56 := (iff #15 #55) -#53 := (iff #14 #45) -#54 := [rewrite]: #53 -#57 := [monotonicity #54]: #56 -#33 := [asserted]: #15 -#60 := [mp #33 #57]: #55 -#153 := (not #143) -#152 := (not #142) -#154 := (or #45 #152 #153) -#155 := [th-lemma]: #154 -[unit-resolution #155 #60 #148 #144]: false -unsat diff -r 344afccb09d1 -r bd4e0d68c56d src/HOL/SMT/Examples/SMT_Examples.certs --- a/src/HOL/SMT/Examples/SMT_Examples.certs Fri Mar 26 23:57:35 2010 +0100 +++ b/src/HOL/SMT/Examples/SMT_Examples.certs Fri Mar 26 23:58:27 2010 +0100 @@ -224,7 +224,7 @@ #30 := [asserted]: #14 [mp #30 #70]: false unsat -c6eb111aa830c9669a030c2e58b4e827706981da 194 0 +212c7825456dae820eef6b1fa0cb8c5ceeff8780 194 0 #2 := false decl up_1 :: bool #4 := up_1 @@ -472,7 +472,7 @@ #113 := [quant-inst]: #199 [unit-resolution #113 #536 #49]: false unsat -94169ba151f7a720e818287ce490015dde764bad 1667 0 +62bff2883948b13c19c4cd52ed250bf0afc3ec90 1667 0 #2 := false decl up_54 :: bool #126 := up_54 @@ -2219,7 +2219,7 @@ #82 := [and-elim #81]: #55 [unit-resolution #82 #95]: false unsat -18bde40beb0dd1fc2613a67805e24d767dd9a3bf 135 0 +bc722e6a73140d95a8643a8d8a522de8bf529dea 135 0 #2 := false decl up_1 :: (-> T1 T2 bool) #5 := (:var 0 T2) @@ -2355,7 +2355,8 @@ #176 := [quant-inst]: #538 [unit-resolution #176 #252 #535]: false unsat -013861f683c286a3ef38681266913846a3a39b9a 135 2 +3ad10572aa4268ecfd73368c6cc15680136648a3 136 0 +WARNING: failed to find a pattern for quantifier (quantifier id: k!12) #2 := false decl up_1 :: (-> T1 T2 bool) #5 := (:var 0 T2) @@ -2491,8 +2492,6 @@ #235 := [quant-inst]: #597 [unit-resolution #235 #311 #594]: false unsat -WARNING: failed to find a pattern for quantifier (quantifier id: k!12) - 0e958e27514643bb596851e6dbb61a23f6b348b0 56 0 #2 := false decl up_1 :: (-> T1 bool) @@ -2942,7 +2941,7 @@ #294 := [unit-resolution #190 #293]: #188 [th-lemma #280 #294]: false unsat -8e6af261ea9f94b967813d4e2f2abcb94463d612 124 0 +a67db8da0b1a1104d4370e2e261e8521096f24e1 124 0 #2 := false decl uf_1 :: (-> T1 T2) decl uf_3 :: T1 @@ -3222,7 +3221,7 @@ #25 := [asserted]: #9 [mp #25 #49]: false unsat -5f3503ae4a43341932052006638f286bea551e87 45 0 +7a45124c81166760c08802d05bb1a73c01b0f138 45 0 #2 := false #11 := 4::real decl uf_2 :: real @@ -3268,7 +3267,7 @@ #60 := [mp #36 #59]: #51 [th-lemma #60 #47 #38]: false unsat -347776ce17d7d3f6d1252ead05795e4eee6f4b20 59 0 +f946ff901958cea1a0225dfba1e556060c889a10 59 0 #2 := false #16 := (not false) decl uf_2 :: int @@ -3328,7 +3327,7 @@ #34 := [asserted]: #18 [mp #34 #71]: false unsat -f7b1b99e3470f713e48aaae1336ace10223be6f0 212 0 +88d529b1517abb78e220ec8f58e3b3405bb2453b 212 0 #2 := false decl uf_4 :: T1 #13 := uf_4 @@ -3628,7 +3627,7 @@ #99 := [unit-resolution #77 #98 #91 #82]: #54 [unit-resolution #99 #112]: false unsat -9791139ea2cfda88ae799477fc61e411aab42b18 673 0 +d4ecdf21a3d5d758670676ddb9e6e093ea9fcc15 673 0 #2 := false #169 := 0::int decl uf_2 :: int @@ -4302,7 +4301,7 @@ #410 := [mp #349 #409]: #405 [unit-resolution #410 #710 #709 #697 #706]: false unsat -0d07e457c5602ba4a5dc70af32b6dc53a80a858c 2291 0 +efea5b71ce31ca68241e4ee8755a8335445d88e6 2291 0 #2 := false #6 := 0::int decl z3name!0 :: int @@ -6881,7 +6880,7 @@ #126 := [mp #101 #125]: #115 [unit-resolution #126 #132 #129]: false unsat -c8ed8eae868ac61c8f3a616f1b0b1df4032f4eac 208 0 +8bded5c2f0cd48cce9a86100cc4c6ce26ec88a2e 208 0 #2 := false #9 := 0::int #11 := 4::int @@ -7646,7 +7645,8 @@ #167 := [unit-resolution #154 #90]: #166 [unit-resolution #167 #165 #162]: false unsat -b7c4f9440c4594c46eee14ce57f17610bb7e2536 83 2 +b7c4f9440c4594c46eee14ce57f17610bb7e2536 84 0 +WARNING: failed to find a pattern for quantifier (quantifier id: k!2) #2 := false #5 := 0::int #4 := (:var 0 int) @@ -7730,9 +7730,8 @@ #62 := [mp~ #54 #61]: #49 [unit-resolution #62 #174]: false unsat +7a9cc3ee85422788d981af84d181bd61d65f774c 181 0 WARNING: failed to find a pattern for quantifier (quantifier id: k!2) - -7a9cc3ee85422788d981af84d181bd61d65f774c 180 2 #2 := false #4 := 0::int #5 := (:var 0 int) @@ -7913,8 +7912,6 @@ #585 := [unit-resolution #128 #581]: #55 [unit-resolution #585 #307]: false unsat -WARNING: failed to find a pattern for quantifier (quantifier id: k!2) - 5201b12abd6b3d0f247a34c1fd9f443fc951c55f 68 0 #2 := false #12 := 1::int @@ -8568,7 +8565,7 @@ #32 := [asserted]: #16 [mp #32 #74]: false unsat -99d65e323e3d85dbdc2d8c52c169db4d46ead198 141 0 +a89308e99854a72f032798efa6ed32cee1f069ad 141 0 #2 := false decl uf_4 :: int #9 := uf_4 @@ -10479,7 +10476,7 @@ #361 := [unit-resolution #639 #655]: #647 [th-lemma #656 #361 #261]: false unsat -980ba021fe0853c3aa46377383e3f0f6fa9e2888 557 0 +201224fffb303874a019c931bc3ddb7a48e74843 557 0 #2 := false #9 := 0::int decl uf_2 :: (-> T1 int) @@ -11131,9 +11128,9 @@ #287 := [th-lemma]: #627 [unit-resolution #287 #47 #635]: false unsat -2e4bd6e1ab7bfedbefd3ada8caf5332ba5651065 1 0 -unsat -96d2e1aad559535e781a07ee5e55bb19caef769c 50 0 +585c02dc1784e4298147af8e1f7a14d1e20f4938 1 0 +unsat +af0e29f90d51c2b97a1ecaa16facf1cd8b6c5ba3 50 0 #2 := false decl uf_6 :: T2 #23 := uf_6 @@ -11184,7 +11181,7 @@ #66 := [asserted]: #26 [unit-resolution #66 #235]: false unsat -008ad82b0a62ff600e66e8f2cc72b5795c7c5032 105 0 +dda7f93ea68b6650d60fb96e3a60e68637d12660 105 0 #2 := false decl uf_6 :: (-> T4 T2) decl uf_10 :: T4 @@ -11290,7 +11287,7 @@ #110 := [asserted]: #46 [unit-resolution #110 #238]: false unsat -0a15a60660bc0c3f06688ad5de50ed50a24d0df0 181 0 +bab035487a4c595c2090c8097591bd8874c90db9 181 0 #2 := false decl uf_1 :: (-> T1 T2 T3) decl uf_3 :: T2 @@ -11472,7 +11469,7 @@ #76 := [asserted]: #38 [unit-resolution #76 #489]: false unsat -dde2364f13fc9ce8af00c7a02bfea9a6c979a805 62 0 +4e1c8dc2fbb6a09931090ee5acf8d0e6f34352b4 62 0 #2 := false decl up_4 :: (-> T1 T2 bool) decl uf_3 :: T2 @@ -11535,7 +11532,7 @@ #73 := [unit-resolution #71 #68]: #72 [unit-resolution #73 #59 #61]: false unsat -3cb6787c7063b0a04bff9e2bfa4203b73903dabe 115 0 +87c5323638926f09820cf502a43fcd61cba03c0c 115 0 #2 := false decl up_2 :: (-> T2 bool) decl uf_3 :: T2 @@ -11651,7 +11648,7 @@ #560 := [mp #344 #559]: #557 [unit-resolution #560 #576 #561]: false unsat -dcb635ada6f2482ea11de30713fe962bcb57c9ad 464 0 +352491b756faec7ffa24a6d9cce95d2879223e60 464 0 #2 := false decl uf_2 :: (-> T2 T3 T3) decl uf_4 :: T3 @@ -12138,7 +12135,7 @@ #25 := [asserted]: #9 [mp #25 #34]: false unsat -f6e9645ebbb8739d12b8e96bc83ddef33c7d53bc 366 0 +c5b3c6b4f593e27f97db06f2c64fc61d8f9bebaa 366 0 #2 := false decl uf_1 :: (-> int T1) #37 := 6::int @@ -12505,7 +12502,7 @@ #182 := [asserted]: #40 [unit-resolution #182 #399]: false unsat -b15b527236338a437e355afcde07dd3c6dfc451f 408 0 +9d577a545efebaa46a634487a3e922a7cddbb866 408 0 #2 := false #22 := 0::int #8 := 2::int @@ -12914,7 +12911,7 @@ #375 := [unit-resolution #374 #407]: #708 [th-lemma #375 #370 #465]: false unsat -71b79533f46a8514b2fc189fc382867d50f52a9a 50 0 +af6e260cca3c1cafcab25bb9a90bb548b2b7ec6b 50 0 #2 := false decl up_35 :: (-> int bool) #112 := 1::int @@ -12965,7 +12962,7 @@ #504 := [quant-inst]: #503 [unit-resolution #504 #916 #297]: false unsat -e40ba7aed8ae5409337a331038da0587c03354d6 506 0 +679f514494fa97481f8fb2124de829ed6e4d2b68 506 0 #2 := false decl uf_17 :: (-> T8 T3) decl uf_18 :: (-> T1 T8)