diff --git a/creusot-deps.opam b/creusot-deps.opam index 903d1ddb7..896c89438 100644 --- a/creusot-deps.opam +++ b/creusot-deps.opam @@ -4,8 +4,8 @@ opam-version: "2.0" maintainer: "Armaël Guéneau " authors: "the creusot authors" depends: [ - "why3" {= "git-5d13"} - "why3-ide" {= "git-5d13" & !?in-creusot-ci} + "why3" {= "git-91b3"} + "why3-ide" {= "git-91b3" & !?in-creusot-ci} # optional dependencies of why3 "ocamlgraph" "camlzip" @@ -16,6 +16,6 @@ depends: [ # When updating the hash and git-XXX below, don't forget to update them in the # depends: field above! pin-depends: [ - [ "why3.git-5d13" "git+https://gitlab.inria.fr/why3/why3.git#5d13eab26ed" ] - [ "why3-ide.git-5d13" "git+https://gitlab.inria.fr/why3/why3.git#5d13eab26ed" ] + [ "why3.git-91b3" "git+https://gitlab.inria.fr/why3/why3.git#91b314fb2" ] + [ "why3-ide.git-91b3" "git+https://gitlab.inria.fr/why3/why3.git#91b314fb2" ] ] diff --git a/creusot-setup/src/tools_versions_urls.rs b/creusot-setup/src/tools_versions_urls.rs index c1621b46c..f4ace251d 100644 --- a/creusot-setup/src/tools_versions_urls.rs +++ b/creusot-setup/src/tools_versions_urls.rs @@ -6,7 +6,7 @@ // - update the SHA256 hash for each binary accordingly (use e.g. sha256sum to compute it) // tools without binary releases -pub const WHY3_VERSION: &'static str = "1.7.1"; +pub const WHY3_VERSION: &'static str = "1.7.2"; pub const ALTERGO_VERSION: &'static str = "2.5.3"; // tools with binary releases pub const Z3_VERSION: &'static str = "4.12.4"; diff --git a/creusot/tests/should_succeed/red_black_tree/why3session.xml b/creusot/tests/should_succeed/red_black_tree/why3session.xml index a783d468d..8f60d1eee 100644 --- a/creusot/tests/should_succeed/red_black_tree/why3session.xml +++ b/creusot/tests/should_succeed/red_black_tree/why3session.xml @@ -10,367 +10,164 @@ - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + @@ -379,31 +176,31 @@ - + - + - + - + - + @@ -412,159 +209,20 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -575,454 +233,25 @@ - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + @@ -1030,6 +259,23 @@ + + + + + + + + + + + + + + + + + @@ -1037,123 +283,107 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - + - - - - - + @@ -1162,20 +392,12 @@ - - - - - - - - - + - + @@ -1184,52 +406,32 @@ - - - - - + - - - - - + - - - - - + - - - - - + - - - - - + - + @@ -1238,16 +440,12 @@ - - - - - + - + @@ -1258,22 +456,14 @@ - - - - - - - - - + - + @@ -1284,16 +474,12 @@ - - - - - + - + @@ -1304,16 +490,12 @@ - - - - - + - + @@ -1322,23 +504,19 @@ - - - - - + - + - + @@ -1347,152 +525,124 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - + + + + - - - - - - + + - - - - + - + - + - - - - - - - - - + - - - - - + - - - - - + @@ -1501,24 +651,12 @@ - - - - - - - - - + - - - - - + @@ -1527,14 +665,10 @@ - + - - - - - + @@ -1543,212 +677,153 @@ - + - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - - - - - - - - + - - - - - - - - - - - - + - + - + - - - - - - - - - - - - - - - - - - - + - + - + @@ -1757,242 +832,145 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - + - + - + - + - + - - - - - - - - + - + - + - - - - - - - - - - - - - - - + - - - - - - - - + - - - - - - - - + - - - - - - - - + - + - + - + - + - - - - - - - - + - + @@ -2001,64 +979,25 @@ - - - - - - - - + - - - - - - - - + - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - + @@ -2067,115 +1006,48 @@ - - - - - - - - - - - - - - - - - - - - + - + - + - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - - - + - + - - - - - - - - - - - - - - - + @@ -2184,40 +1056,15 @@ - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - + @@ -2226,33 +1073,22 @@ - - - - - - - - - - - - + - + - + - + @@ -2263,29 +1099,15 @@ - - - - - - - - + - - - - - - - - + - + @@ -2294,29 +1116,22 @@ - - - - - - - - + - + - + - + @@ -2325,105 +1140,90 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - - - - - - - - - - - - + @@ -2432,15 +1232,15 @@ - + - + - + @@ -2449,240 +1249,164 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - + - + - + - + - + - + - - - - - - - - - - - - + - + - + - + - + - + - + - - - - - + - - - - - - - - - - - - - - - - + - + - + - - - - - - - - - + - - - - - - - - - - - - - - - - + - - - - - - - - - + - + - - - - - - - - - - - - + @@ -2693,23 +1417,19 @@ - + - + - - - - - + @@ -2718,19 +1438,19 @@ - + - + - + @@ -2741,7 +1461,7 @@ - + @@ -2750,16 +1470,12 @@ - + - - - - - + @@ -2768,13 +1484,27 @@ - + + + + + + + + + + + + + + + - + - + @@ -2783,156 +1513,84 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - + @@ -2941,15 +1599,15 @@ - + - + - + @@ -2958,111 +1616,107 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -3071,25 +1725,21 @@ - + - + - + - + - - - - - + @@ -3100,211 +1750,153 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - + - + - + - + - + - + - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - + @@ -3317,10 +1909,10 @@ - + - + @@ -3333,15 +1925,7 @@ - - - - - - - - - + @@ -3352,110 +1936,48 @@ - - - - - - - - - - - - + - - - - - + - + - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - + + + + - - - - - + - - - - - - - - + - + - + - + - - - - - + - + @@ -3464,31 +1986,27 @@ - + - - - - - + - + - + - + @@ -3501,43 +2019,21 @@ - - - - - + - + - - - - - - - - - - - - + - + - - - - - - - - + @@ -3548,47 +2044,35 @@ - + - + - - - - - + - - - - - + - - - - - + - + - + @@ -3601,36 +2085,21 @@ - + - + - - - - - - - - - - - - - - - - + - + - + @@ -3639,59 +2108,21 @@ - - - - - + - + - - - - - - - - - - - - - - - - - - - - + - + - - - - - - - - - - - - - - - - + @@ -3704,10 +2135,10 @@ - + - + @@ -3716,129 +2147,31 @@ - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - + @@ -3851,49 +2184,25 @@ - - - - - - - - - + - + - - - - - - - - - - - - - - - - - + - + - + @@ -3902,29 +2211,14 @@ - - - - - - - - - - - - + - - - - - + @@ -3935,20 +2229,12 @@ - - - - - - - - - + - + @@ -3959,23 +2245,19 @@ - + - - - - - + - + @@ -3984,16 +2266,12 @@ - + - - - - - + @@ -4006,71 +2284,39 @@ - - - - - - - - - - - - - + - + - - - - - + - - - - - + - - - - - - - - - - - - - + - + - + @@ -4083,48 +2329,28 @@ - - - - - + - + - + - - - - - - - - - - - - - - - - - + - + - + @@ -4133,190 +2359,90 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - + @@ -4327,164 +2453,138 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - + @@ -4495,7 +2595,7 @@ - + @@ -4504,46 +2604,27 @@ - + - + - - - - - - - - - - - - - - - - - - - - + - + - + diff --git a/creusot/tests/should_succeed/red_black_tree/why3shapes.gz b/creusot/tests/should_succeed/red_black_tree/why3shapes.gz index ca8a8e6cf..c4f27b586 100644 Binary files a/creusot/tests/should_succeed/red_black_tree/why3shapes.gz and b/creusot/tests/should_succeed/red_black_tree/why3shapes.gz differ