Fix tests

creusot/tests/should_fail/bug/436_0.rs

@@ -2,16 +2,16 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 struct S {
-    g: Snapshot<i32>,
+    g: Snapshot<Int>,
 }
 
 #[logic(prophetic)]
-fn prophecy(x: &mut S) -> i32 {
+fn prophecy(x: &mut S) -> Int {
     pearlite! { *(^x).g }
 }
 
 pub fn f() {
-    let b = &mut S { g: snapshot! { 1i32 } };
-    b.g = snapshot! { prophecy(b) + 1i32 };
+    let b = &mut S { g: snapshot! { 1 } };
+    b.g = snapshot! { prophecy(b) + 1 };
     proof_assert! { false }
 }

creusot/tests/should_succeed/bug/545.rs

@@ -2,5 +2,5 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 pub fn negative_is_negative() {
-    proof_assert!(0i32 > -100i32);
+    proof_assert!(0 > -100);
 }

creusot/tests/should_succeed/bug/682.rs

@@ -1,7 +1,7 @@
 extern crate creusot_contracts;
 use creusot_contracts::*;
 
-#[requires(*a <= u64::MAX / 2u64)]
+#[requires((*a)@ <= u64::MAX / 2u64)]
 #[ensures(^a > *a)]
 fn add_some(a: &mut u64) {
     *a += 1;

creusot/tests/should_succeed/cell/01.rs

@@ -33,7 +33,7 @@ impl Inv<u32> for Even {
     #[open]
     #[predicate]
     fn inv(x: u32) -> bool {
-        x % 2u32 == 0u32
+        x.view() % 2 == 0
     }
 }
 

creusot/tests/should_succeed/list_reversal_lasso.rs

@@ -2,7 +2,7 @@
 
 extern crate creusot_contracts;
 
-use creusot_contracts::{logic::IndexLogic, *};
+use creusot_contracts::{logic::ops::IndexLogic, *};
 use std::ops::{Index, IndexMut};
 
 /* Memory model */

creusot/tests/should_succeed/mc91.rs

@@ -3,7 +3,7 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 #[ensures(x <= 100u32 ==> result == 91u32 &&
-    x > 100u32 ==> result == x - 10u32)]
+    x > 100u32 ==> result@ == x - 10u32)]
 pub fn mc91(x: u32) -> u32 {
     if x > 100 {
         x - 10

creusot/tests/should_succeed/mutex.rs

@@ -64,7 +64,7 @@ impl Inv<u32> for Even {
     #[open(self)]
     #[predicate]
     fn inv(&self, x: u32) -> bool {
-        x % 2u32 == 0u32
+        x.view() % 2 == 0
     }
 }