Update tests

Author: voidc

creusot/tests/should_fail/bug/692.mlcfg

@@ -417,9 +417,11 @@ end
 module Core_Ops_Range_Range_Type_Inv
   type idx
   use Core_Ops_Range_Range_Type as Core_Ops_Range_Range_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = idx
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
     type t = Core_Ops_Range_Range_Type.t_range idx
-  axiom inv_t_range : forall self : Core_Ops_Range_Range_Type.t_range idx . Inv0.inv self = true
+  axiom inv_t_range [@rewrite] : forall self : Core_Ops_Range_Range_Type.t_range idx . Inv0.inv self = (Inv1.inv (Core_Ops_Range_Range_Type.range_start self) /\ Inv1.inv (Core_Ops_Range_Range_Type.range_end self))
 end
 module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
   type self
@@ -997,6 +999,12 @@ module CreusotContracts_Std1_Slice_Impl5_ResolveElswhere
     ensures { result = resolve_elswhere self old' fin }
 
 end
+module TyInv_Trivial
+  type t
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = t
+  axiom inv_trivial : forall self : t . Inv0.inv self = true
+end
 module C100doors_F_Interface
   val f [#"../100doors.rs" 18 0 18 10] (_1 : ()) : ()
 end
@@ -1006,6 +1014,12 @@ module C100doors_F
   use prelude.Ghost
   use seq.Seq
   use prelude.Borrow
+  clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
+    type t = usize
+  clone TyInv_Trivial as TyInv_Trivial0 with
+    type t = usize,
+    predicate Inv0.inv = Inv1.inv,
+    axiom .
   clone CreusotContracts_Std1_Slice_Impl5_ResolveElswhere as ResolveElswhere0 with
     type t = bool
   use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
@@ -1056,6 +1070,7 @@ module C100doors_F
   clone Core_Ops_Range_Range_Type_Inv as Core_Ops_Range_Range_Type_Inv0 with
     type idx = usize,
     predicate Inv0.inv = Inv0.inv,
+    predicate Inv1.inv = Inv1.inv,
     axiom .
   clone CreusotContracts_Std1_Iter_Impl0_IntoIterPost as IntoIterPost0 with
     type i = Core_Ops_Range_Range_Type.t_range usize

creusot/tests/should_fail/bug/695.mlcfg

@@ -7,7 +7,7 @@
 <path name=".."/><path name="100doors.mlcfg"/>
 <theory name="C100doors_F" proved="true">
  <goal name="f&#39;vc" expl="VC for f" proved="true">
- <proof prover="1"><result status="valid" time="0.220000" steps="45466"/></proof>
+ <proof prover="1"><result status="valid" time="0.220000" steps="49042"/></proof>
  </goal>
 </theory>
 </file>

creusot/tests/should_succeed/100doors.mlcfg

@@ -2043,9 +2043,11 @@ end
 module Core_Ops_Range_Range_Type_Inv
   type idx
   use Core_Ops_Range_Range_Type as Core_Ops_Range_Range_Type
+  clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
+    type t = idx
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
     type t = Core_Ops_Range_Range_Type.t_range idx
-  axiom inv_t_range : forall self : Core_Ops_Range_Range_Type.t_range idx . Inv0.inv self = true
+  axiom inv_t_range [@rewrite] : forall self : Core_Ops_Range_Range_Type.t_range idx . Inv0.inv self = (Inv1.inv (Core_Ops_Range_Range_Type.range_start self) /\ Inv1.inv (Core_Ops_Range_Range_Type.range_end self))
 end
 module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
   type self
@@ -2319,6 +2321,12 @@ module CreusotContracts_Std1_Iter_Range_Impl0_Completed
     ensures { result = completed self }
 
 end
+module TyInv_Trivial
+  type t
+  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
+    type t = t
+  axiom inv_trivial : forall self : t . Inv0.inv self = true
+end
 module Hillel_Unique_Interface
   type t
   use prelude.Borrow
@@ -2372,6 +2380,12 @@ module Hillel_Unique
   use seq_ext.SeqExt
   use prelude.Borrow
   use prelude.Slice
+  clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
+    type t = usize
+  clone TyInv_Trivial as TyInv_Trivial0 with
+    type t = usize,
+    predicate Inv0.inv = Inv1.inv,
+    axiom .
   use seq.Seq
   clone Core_Num_Impl11_Max as Max0
   clone CreusotContracts_Std1_Slice_Impl0_ShallowModel_Interface as ShallowModel2 with
@@ -2446,6 +2460,7 @@ module Hillel_Unique
   clone Core_Ops_Range_Range_Type_Inv as Core_Ops_Range_Range_Type_Inv0 with
     type idx = usize,
     predicate Inv0.inv = Inv0.inv,
+    predicate Inv1.inv = Inv1.inv,
     axiom .
   clone CreusotContracts_Std1_Iter_Impl0_IntoIterPost as IntoIterPost0 with
     type i = Core_Ops_Range_Range_Type.t_range usize
@@ -2957,6 +2972,12 @@ module Hillel_Fulcrum
   use prelude.Borrow
   use prelude.UIntSize
   use prelude.Slice
+  clone CreusotContracts_Invariant_Inv_Interface as Inv2 with
+    type t = usize
+  clone TyInv_Trivial as TyInv_Trivial0 with
+    type t = usize,
+    predicate Inv0.inv = Inv2.inv,
+    axiom .
   use Core_Slice_Iter_Iter_Type as Core_Slice_Iter_Iter_Type
   clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Interface as ShallowModel1 with
     type t = uint32
@@ -2996,6 +3017,7 @@ module Hillel_Fulcrum
   clone Core_Ops_Range_Range_Type_Inv as Core_Ops_Range_Range_Type_Inv0 with
     type idx = usize,
     predicate Inv0.inv = Inv1.inv,
+    predicate Inv1.inv = Inv2.inv,
     axiom .
   clone CreusotContracts_Std1_Iter_Impl0_IntoIterPost as IntoIterPost1 with
     type i = Core_Ops_Range_Range_Type.t_range usize