Update tests

Author: arnaudgolfouse

tests/creusot-contracts/creusot-contracts.coma

@@ -20,7 +20,7 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs"
   let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
   let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
   let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
-  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
+  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
   let%span smodel = "../../../creusot-contracts/src/model.rs" 63 8 63 22
 
   use creusot.prelude.Opaque

tests/creusot-contracts/creusot-contracts/why3session.xml

@@ -1,10 +1,13 @@
 module M_1204__evil [#"1204.rs" 8 0 8 26]
-  let%span s1204 = "1204.rs" 6 11 6 16
-  let%span s1204'0 = "1204.rs" 7 10 7 11
+  let%span s1204 = "1204.rs" 7 10 7 11
+  let%span s1204'0 = "1204.rs" 6 11 6 16
   let%span s1204'1 = "1204.rs" 9 4 9 16
+  let%span swell_founded = "../../../creusot-contracts/src/logic/well_founded.rs" 45 8 45 33
 
   use mach.int.Int
 
+  predicate well_founded_relation (self: int) (other: int) = [%#swell_founded] self >= 0 /\ self > other
+  
   meta "compute_max_steps" 1000000
 
   meta "select_lsinst" "all"
@@ -13,14 +16,14 @@ module M_1204__evil [#"1204.rs" 8 0 8 26]
 
   function evil [#"1204.rs" 8 0 8 26] (x'0: int) : int
 
-  goal vc_evil: ([%#s1204] false)
-    -> ([@expl:evil requires] [%#s1204] false) /\ 0 <= ([%#s1204'0] x) /\ ([%#s1204'0] - x) < ([%#s1204'0] x)
+  goal vc_evil: ([%#s1204'0] false)
+    -> ([@expl:evil requires] [%#s1204'0] false) /\ well_founded_relation ([%#s1204] x) ([%#s1204] - x)
 end
 module M_1204__wrong [#"1204.rs" 14 0 14 14]
   let%span s1204 = "1204.rs" 13 10 13 15
   let%span s1204'0 = "1204.rs" 6 11 6 16
-  let%span s1204'1 = "1204.rs" 7 10 7 11
-  let%span s1204'2 = "1204.rs" 15 4 15 43
+  let%span s1204'1 = "1204.rs" 15 4 15 43
+  let%span s1204'2 = "1204.rs" 7 10 7 11
   let%span s1204'3 = "1204.rs" 9 4 9 16
 
   use mach.int.Int

tests/creusot-contracts/creusot-contracts/why3shapes.gz

@@ -130,7 +130,7 @@ module M_692__valid_normal [#"692.rs" 12 0 12 34]
   let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
   let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
   let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
-  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
+  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
   let%span sresolve = "../../../creusot-contracts/src/resolve.rs" 52 20 52 34
 
   use creusot.int.UInt32

tests/should_fail/bug/01_resolve_unsoundness.coma

@@ -171,7 +171,7 @@ module M_695__valid [#"695.rs" 12 0 12 27]
   let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
   let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
   let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
-  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
+  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
   let%span sresolve = "../../../creusot-contracts/src/resolve.rs" 52 20 52 34
 
   use creusot.int.UInt32

tests/should_fail/bug/1204.coma

@@ -18,10 +18,10 @@ module M_generic_deref_ghost__deref_wrap [#"generic_deref_ghost.rs" 8 0 8 48]
 
   use creusot.prelude.Any
 
-  type t_Target
-  
   type t_T
 
+  type t_Target
+  
   predicate precondition (self: ()) (args: t_T)
 
   axiom precondition_fndef: