Adjust ui tests

creusot/tests/should_fail/bug/222.mlcfg

@@ -259,7 +259,7 @@ module C222_UsesInvariant
   }
   BB0 {
     _5 <- Borrow.borrow_mut (C222_Once_Type.once_0 ( * x));
-    x <- { x with current = (let C222_Once_Type.C_Once a =  * x in C222_Once_Type.C_Once ( ^ _5)) };
+    x <- Borrow.make_borrow (let C222_Once_Type.C_Once a =  * x in C222_Once_Type.C_Once ( ^ _5)) ( ^ x);
     assume { Inv0.inv ( ^ _5) };
     _4 <- ([#"../222.rs" 41 4 41 14] Take0.take _5);
     _5 <- any borrowed (Core_Option_Option_Type.t_option t);

creusot/tests/should_fail/bug/492.mlcfg

@@ -100,7 +100,7 @@ module C492_ReborrowTuple
   }
   BB0 {
     _3 <- Borrow.borrow_mut ( * x);
-    x <- { x with current = ( ^ _3) };
+    x <- Borrow.make_borrow ( ^ _3) ( ^ x);
     assume { Inv0.inv ( ^ _3) };
     _0 <- (_3, [#"../492.rs" 6 8 6 10] (32 : uint32));
     _3 <- any borrowed t;
@@ -226,7 +226,7 @@ module C492_Test
     _6 <- Borrow.borrow_mut x;
     x <-  ^ _6;
     _5 <- Borrow.borrow_mut ( * _6);
-    _6 <- { _6 with current = ( ^ _5) };
+    _6 <- Borrow.make_borrow ( ^ _5) ( ^ _6);
     _4 <- ([#"../492.rs" 12 19 12 41] ReborrowTuple0.reborrow_tuple _5);
     _5 <- any borrowed int32;
     goto BB1
@@ -237,7 +237,7 @@ module C492_Test
     assume { Resolve0.resolve _4 };
     assume { Resolve1.resolve _6 };
     assert { [@expl:assertion] [#"../492.rs" 13 18 13 30]  ^ res = (5 : int32) };
-    res <- { res with current = ([#"../492.rs" 14 11 14 13] (10 : int32)) };
+    res <- Borrow.make_borrow ([#"../492.rs" 14 11 14 13] (10 : int32)) ( ^ res);
     assume { Resolve1.resolve res };
     _0 <- ();
     return _0

creusot/tests/should_fail/bug/692.mlcfg

@@ -942,7 +942,7 @@ module C692_ValidNormal_Closure2
     goto BB3
   }
   BB3 {
-    _1 <- { _1 with current = (let C692_ValidNormal_Closure2 a =  * _1 in C692_ValidNormal_Closure2 ({ (field_0 ( * _1)) with current = _4 })) };
+    _1 <- Borrow.make_borrow (let C692_ValidNormal_Closure2 a =  * _1 in C692_ValidNormal_Closure2 (Borrow.make_borrow _4 ( ^ field_0 ( * _1)))) ( ^ _1);
     _4 <- any uint32;
     assume { Resolve0.resolve _1 };
     res <- ();

creusot/tests/should_fail/bug/695.mlcfg

@@ -1142,7 +1142,7 @@ module C695_Valid_Closure2
     goto BB3
   }
   BB3 {
-    _1 <- { _1 with current = (let C695_Valid_Closure2 a =  * _1 in C695_Valid_Closure2 ({ (field_0 ( * _1)) with current = _4 })) };
+    _1 <- Borrow.make_borrow (let C695_Valid_Closure2 a =  * _1 in C695_Valid_Closure2 (Borrow.make_borrow _4 ( ^ field_0 ( * _1)))) ( ^ _1);
     _4 <- any uint32;
     assume { Resolve0.resolve _1 };
     res <- ();

creusot/tests/should_succeed/100doors.mlcfg

@@ -1361,7 +1361,7 @@ module C100doors_F
     _14 <- Borrow.borrow_mut iter;
     iter <-  ^ _14;
     _13 <- Borrow.borrow_mut ( * _14);
-    _14 <- { _14 with current = ( ^ _13) };
+    _14 <- Borrow.make_borrow ( ^ _13) ( ^ _14);
     _12 <- ([#"../100doors.rs" 20 4 20 41] Next0.next _13);
     _13 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize);
     goto BB8
@@ -1423,7 +1423,7 @@ module C100doors_F
     goto BB19
   }
   BB19 {
-    _30 <- { _30 with current = (not _26) };
+    _30 <- Borrow.make_borrow (not _26) ( ^ _30);
     assume { Resolve1.resolve _30 };
     door <- ([#"../100doors.rs" 27 12 27 24] door + pass);
     _11 <- ();

creusot/tests/should_succeed/100doors/why3session.xml

@@ -2,12 +2,12 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="1" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.8.12" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
 <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.327048" steps="945633"/></proof>
+ <proof prover="0"><result status="valid" time="0.327048" steps="557345"/></proof>
  </goal>
 </theory>
 </file>

creusot/tests/should_succeed/all_zero.mlcfg

@@ -173,13 +173,13 @@ module AllZero_AllZero
   }
   BB5 {
     value <- Borrow.borrow_mut (AllZero_List_Type.cons_0 ( * loop_l));
-    loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons a b =  * loop_l in AllZero_List_Type.C_Cons ( ^ value) b) };
+    loop_l <- Borrow.make_borrow (let AllZero_List_Type.C_Cons a b =  * loop_l in AllZero_List_Type.C_Cons ( ^ value) b) ( ^ loop_l);
     next <- Borrow.borrow_mut (AllZero_List_Type.cons_1 ( * loop_l));
-    loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons a b =  * loop_l in AllZero_List_Type.C_Cons a ( ^ next)) };
-    value <- { value with current = ([#"../all_zero.rs" 44 17 44 18] (0 : uint32)) };
+    loop_l <- Borrow.make_borrow (let AllZero_List_Type.C_Cons a b =  * loop_l in AllZero_List_Type.C_Cons a ( ^ next)) ( ^ loop_l);
+    value <- Borrow.make_borrow ([#"../all_zero.rs" 44 17 44 18] (0 : uint32)) ( ^ value);
     assume { Resolve0.resolve value };
     _13 <- Borrow.borrow_mut ( * next);
-    next <- { next with current = ( ^ _13) };
+    next <- Borrow.make_borrow ( ^ _13) ( ^ next);
     assume { Resolve1.resolve loop_l };
     loop_l <- _13;
     _13 <- any borrowed (AllZero_List_Type.t_list);

creusot/tests/should_succeed/all_zero/why3session.xml

@@ -2,12 +2,12 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
 <path name=".."/><path name="all_zero.mlcfg"/>
 <theory name="AllZero_AllZero" proved="true">
  <goal name="all_zero&#39;vc" expl="VC for all_zero" proved="true">
- <proof prover="1"><result status="valid" time="0.038573" steps="808"/></proof>
+ <proof prover="0"><result status="valid" time="0.038573" steps="806"/></proof>
  </goal>
 </theory>
 </file>

creusot/tests/should_succeed/bdd.mlcfg

@@ -3024,7 +3024,7 @@ module Bdd_Impl11_Hashcons
     r1 <- Bdd_Bdd_Type.C_Bdd ( * _19) (Bdd_Context_Type.context_cnt ( * self));
     assume { Resolve1.resolve _19 };
     _24 <- Borrow.borrow_mut (Bdd_Context_Type.context_hashcons ( * self));
-    self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a ( ^ _24) c d e f) };
+    self <- Borrow.make_borrow (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a ( ^ _24) c d e f) ( ^ self);
     _23 <- ([#"../bdd.rs" 446 8 446 31] Add0.add _24 n r1);
     _24 <- any borrowed (Bdd_Hashmap_MyHashMap_Type.t_myhashmap (Bdd_Node_Type.t_node) (Bdd_Bdd_Type.t_bdd));
     goto BB6
@@ -3034,7 +3034,7 @@ module Bdd_Impl11_Hashcons
     goto BB7
   }
   BB7 {
-    self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b _27 d e f) };
+    self <- Borrow.make_borrow (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b _27 d e f) ( ^ self);
     _27 <- any Ghost.ghost_ty (Map.map uint64 (Bdd_Node_Type.t_node));
     switch ([#"../bdd.rs" 448 11 448 34] Bdd_Context_Type.context_cnt ( * self) > ([#"../bdd.rs" 448 22 448 34] ([#"../bdd.rs" 448 22 448 30] (18446744073709551615 : uint64)) - ([#"../bdd.rs" 448 33 448 34] (1 : uint64))))
       | False -> goto BB11
@@ -3048,11 +3048,11 @@ module Bdd_Impl11_Hashcons
     goto BB10
   }
   BB10 {
-    self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d e (Bdd_Context_Type.context_cnt ( * self))) };
+    self <- Borrow.make_borrow (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d e (Bdd_Context_Type.context_cnt ( * self))) ( ^ self);
     goto BB9
   }
   BB11 {
-    self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d e ([#"../bdd.rs" 454 8 454 21] Bdd_Context_Type.context_cnt ( * self) + ([#"../bdd.rs" 454 20 454 21] (1 : uint64)))) };
+    self <- Borrow.make_borrow (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d e ([#"../bdd.rs" 454 8 454 21] Bdd_Context_Type.context_cnt ( * self) + ([#"../bdd.rs" 454 20 454 21] (1 : uint64)))) ( ^ self);
     assert { [@expl:type invariant] Inv0.inv self };
     assume { Resolve0.resolve self };
     _0 <- r1;
@@ -3221,7 +3221,7 @@ module Bdd_Impl11_Node
   }
   BB3 {
     _17 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _17) };
+    self <- Borrow.make_borrow ( ^ _17) ( ^ self);
     assume { Inv0.inv ( ^ _17) };
     _0 <- ([#"../bdd.rs" 469 8 469 50] Hashcons0.hashcons _17 (Bdd_Node_Type.C_If x childt childf));
     _17 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3353,7 +3353,7 @@ module Bdd_Impl11_True
   }
   BB0 {
     _6 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _6) };
+    self <- Borrow.make_borrow ( ^ _6) ( ^ self);
     assume { Inv0.inv ( ^ _6) };
     _0 <- ([#"../bdd.rs" 477 8 477 27] Hashcons0.hashcons _6 (Bdd_Node_Type.C_True));
     _6 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3482,7 +3482,7 @@ module Bdd_Impl11_False
   }
   BB0 {
     _6 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _6) };
+    self <- Borrow.make_borrow ( ^ _6) ( ^ self);
     assume { Inv0.inv ( ^ _6) };
     _0 <- ([#"../bdd.rs" 485 8 485 28] Hashcons0.hashcons _6 (Bdd_Node_Type.C_False));
     _6 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3627,23 +3627,23 @@ module Bdd_Impl11_V
   }
   BB0 {
     _7 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _7) };
+    self <- Borrow.make_borrow ( ^ _7) ( ^ self);
     assume { Inv0.inv ( ^ _7) };
     t <- ([#"../bdd.rs" 492 16 492 28] True0.true_ _7);
     _7 <- any borrowed (Bdd_Context_Type.t_context);
     goto BB1
   }
   BB1 {
     _9 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _9) };
+    self <- Borrow.make_borrow ( ^ _9) ( ^ self);
     assume { Inv0.inv ( ^ _9) };
     f <- ([#"../bdd.rs" 493 16 493 29] False0.false_ _9);
     _9 <- any borrowed (Bdd_Context_Type.t_context);
     goto BB2
   }
   BB2 {
     _10 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _10) };
+    self <- Borrow.make_borrow ( ^ _10) ( ^ self);
     assume { Inv0.inv ( ^ _10) };
     _0 <- ([#"../bdd.rs" 494 8 494 26] Node0.node _10 x t f);
     _10 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3907,15 +3907,15 @@ module Bdd_Impl11_Not
     childt <- Bdd_Node_Type.if_childt (Bdd_Bdd_Type.bdd_0 x);
     childf <- Bdd_Node_Type.if_childf (Bdd_Bdd_Type.bdd_0 x);
     _25 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _25) };
+    self <- Borrow.make_borrow ( ^ _25) ( ^ self);
     assume { Inv1.inv ( ^ _25) };
     childt1 <- ([#"../bdd.rs" 511 29 511 45] not' _25 childt);
     _25 <- any borrowed (Bdd_Context_Type.t_context);
     goto BB13
   }
   BB9 {
     _19 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _19) };
+    self <- Borrow.make_borrow ( ^ _19) ( ^ self);
     assume { Inv1.inv ( ^ _19) };
     r1 <- ([#"../bdd.rs" 508 20 508 33] False0.false_ _19);
     _19 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3926,7 +3926,7 @@ module Bdd_Impl11_Not
   }
   BB11 {
     _20 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _20) };
+    self <- Borrow.make_borrow ( ^ _20) ( ^ self);
     assume { Inv1.inv ( ^ _20) };
     r1 <- ([#"../bdd.rs" 509 21 509 33] True0.true_ _20);
     _20 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3937,15 +3937,15 @@ module Bdd_Impl11_Not
   }
   BB13 {
     _28 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _28) };
+    self <- Borrow.make_borrow ( ^ _28) ( ^ self);
     assume { Inv1.inv ( ^ _28) };
     childf1 <- ([#"../bdd.rs" 512 29 512 45] not' _28 childf);
     _28 <- any borrowed (Bdd_Context_Type.t_context);
     goto BB14
   }
   BB14 {
     _30 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _30) };
+    self <- Borrow.make_borrow ( ^ _30) ( ^ self);
     assume { Inv1.inv ( ^ _30) };
     r1 <- ([#"../bdd.rs" 513 16 513 44] Node0.node _30 v childt1 childf1);
     _30 <- any borrowed (Bdd_Context_Type.t_context);
@@ -3956,7 +3956,7 @@ module Bdd_Impl11_Not
   }
   BB16 {
     _35 <- Borrow.borrow_mut (Bdd_Context_Type.context_not_memo ( * self));
-    self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c ( ^ _35) e f) };
+    self <- Borrow.make_borrow (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c ( ^ _35) e f) ( ^ self);
     _34 <- ([#"../bdd.rs" 516 8 516 31] Add0.add _35 x r1);
     _35 <- any borrowed (Bdd_Hashmap_MyHashMap_Type.t_myhashmap (Bdd_Bdd_Type.t_bdd) (Bdd_Bdd_Type.t_bdd));
     goto BB17
@@ -4548,7 +4548,7 @@ module Bdd_Impl11_And
   BB17 {
     assume { Resolve2.resolve _23 };
     _31 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _31) };
+    self <- Borrow.make_borrow ( ^ _31) ( ^ self);
     assume { Inv1.inv ( ^ _31) };
     r1 <- ([#"../bdd.rs" 534 39 534 52] False0.false_ _31);
     _31 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4570,7 +4570,7 @@ module Bdd_Impl11_And
   BB21 {
     v <- va;
     _67 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _67) };
+    self <- Borrow.make_borrow ( ^ _67) ( ^ self);
     assume { Inv1.inv ( ^ _67) };
     _66 <- ([#"../bdd.rs" 553 33 553 59] and _67 childta childtb);
     _67 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4582,7 +4582,7 @@ module Bdd_Impl11_And
   BB23 {
     v <- vb;
     _49 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _49) };
+    self <- Borrow.make_borrow ( ^ _49) ( ^ self);
     assume { Inv1.inv ( ^ _49) };
     _48 <- ([#"../bdd.rs" 543 33 543 53] and _49 a childtb);
     _49 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4592,7 +4592,7 @@ module Bdd_Impl11_And
     childt <- _48;
     _48 <- any Bdd_Bdd_Type.t_bdd;
     _53 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _53) };
+    self <- Borrow.make_borrow ( ^ _53) ( ^ self);
     assume { Inv1.inv ( ^ _53) };
     _52 <- ([#"../bdd.rs" 544 33 544 53] and _53 a childfb);
     _53 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4607,7 +4607,7 @@ module Bdd_Impl11_And
   BB26 {
     v <- va;
     _58 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _58) };
+    self <- Borrow.make_borrow ( ^ _58) ( ^ self);
     assume { Inv1.inv ( ^ _58) };
     _57 <- ([#"../bdd.rs" 548 33 548 53] and _58 childta b);
     _58 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4617,7 +4617,7 @@ module Bdd_Impl11_And
     childt <- _57;
     _57 <- any Bdd_Bdd_Type.t_bdd;
     _62 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _62) };
+    self <- Borrow.make_borrow ( ^ _62) ( ^ self);
     assume { Inv1.inv ( ^ _62) };
     _61 <- ([#"../bdd.rs" 549 33 549 53] and _62 childfa b);
     _62 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4633,7 +4633,7 @@ module Bdd_Impl11_And
     childt <- _66;
     _66 <- any Bdd_Bdd_Type.t_bdd;
     _71 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _71) };
+    self <- Borrow.make_borrow ( ^ _71) ( ^ self);
     assume { Inv1.inv ( ^ _71) };
     _70 <- ([#"../bdd.rs" 554 33 554 59] and _71 childfa childfb);
     _71 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4647,7 +4647,7 @@ module Bdd_Impl11_And
   }
   BB31 {
     _74 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _74) };
+    self <- Borrow.make_borrow ( ^ _74) ( ^ self);
     assume { Inv1.inv ( ^ _74) };
     r1 <- ([#"../bdd.rs" 557 16 557 44] Node0.node _74 v childt childf);
     _74 <- any borrowed (Bdd_Context_Type.t_context);
@@ -4658,7 +4658,7 @@ module Bdd_Impl11_And
   }
   BB33 {
     _79 <- Borrow.borrow_mut (Bdd_Context_Type.context_and_memo ( * self));
-    self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d ( ^ _79) f) };
+    self <- Borrow.make_borrow (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d ( ^ _79) f) ( ^ self);
     _78 <- ([#"../bdd.rs" 560 8 560 36] Add0.add _79 (a, b) r1);
     _79 <- any borrowed (Bdd_Hashmap_MyHashMap_Type.t_myhashmap (Bdd_Bdd_Type.t_bdd, Bdd_Bdd_Type.t_bdd) (Bdd_Bdd_Type.t_bdd));
     goto BB34

creusot/tests/should_succeed/bug/486.mlcfg

@@ -33,7 +33,7 @@ module C486_Test
     goto BB0
   }
   BB0 {
-    x <- (let C486_HasMutRef_Type.C_HasMutRef a = x in C486_HasMutRef_Type.C_HasMutRef ({ (C486_HasMutRef_Type.hasmutref_0 x) with current = ([#"../486.rs" 8 11 8 12] (5 : uint32)) }));
+    x <- (let C486_HasMutRef_Type.C_HasMutRef a = x in C486_HasMutRef_Type.C_HasMutRef (Borrow.make_borrow ([#"../486.rs" 8 11 8 12] (5 : uint32)) ( ^ C486_HasMutRef_Type.hasmutref_0 x)));
     _0 <- ();
     return _0
   }

creusot/tests/should_succeed/bug/682.mlcfg

@@ -60,7 +60,7 @@ module C682_AddSome
     goto BB0
   }
   BB0 {
-    a <- { a with current = ([#"../682.rs" 7 4 7 11]  * a + ([#"../682.rs" 7 10 7 11] (1 : uint64))) };
+    a <- Borrow.make_borrow ([#"../682.rs" 7 4 7 11]  * a + ([#"../682.rs" 7 10 7 11] (1 : uint64))) ( ^ a);
     assume { Resolve0.resolve a };
     _0 <- ();
     return _0
@@ -105,7 +105,7 @@ module C682_Foo
   }
   BB1 {
     _7 <- Borrow.borrow_mut ( * a);
-    a <- { a with current = ( ^ _7) };
+    a <- Borrow.make_borrow ( ^ _7) ( ^ a);
     _6 <- ([#"../682.rs" 14 4 14 15] AddSome0.add_some _7);
     _7 <- any borrowed uint64;
     goto BB2

creusot/tests/should_succeed/bug/682/why3session.xml

@@ -2,17 +2,17 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
 <path name=".."/><path name="682.mlcfg"/>
 <theory name="C682_AddSome" proved="true">
  <goal name="add_some&#39;vc" expl="VC for add_some" proved="true">
- <proof prover="1"><result status="valid" time="0.012416" steps="196"/></proof>
+ <proof prover="0"><result status="valid" time="0.012416" steps="196"/></proof>
  </goal>
 </theory>
 <theory name="C682_Foo" proved="true">
  <goal name="foo&#39;vc" expl="VC for foo" proved="true">
- <proof prover="1"><result status="valid" time="0.018181" steps="436"/></proof>
+ <proof prover="0"><result status="valid" time="0.018181" steps="438"/></proof>
  </goal>
 </theory>
 </file>

creusot/tests/should_succeed/bug/766.mlcfg

@@ -190,7 +190,7 @@ module C766_Trait_Goo
   }
   BB0 {
     _2 <- Borrow.borrow_mut ( * self);
-    self <- { self with current = ( ^ _2) };
+    self <- Borrow.make_borrow ( ^ _2) ( ^ self);
     assume { Inv0.inv ( ^ _2) };
     _0 <- ([#"../766.rs" 11 8 11 16] F0.f _2);
     _2 <- any borrowed self;