From 7bda0dc7de1e4a0f466040784b4dbd3be8c0e03d Mon Sep 17 00:00:00 2001
From: arnaudgolfouse <arnaud.golfouse@laposte.net>
Date: Tue, 3 Dec 2024 15:46:23 +0100
Subject: [PATCH] Fix tests

---
 creusot/tests/should_fail/bug/436_0.rs              | 8 ++++----
 creusot/tests/should_succeed/bug/545.rs             | 2 +-
 creusot/tests/should_succeed/bug/682.rs             | 2 +-
 creusot/tests/should_succeed/cell/01.rs             | 2 +-
 creusot/tests/should_succeed/list_reversal_lasso.rs | 2 +-
 creusot/tests/should_succeed/mc91.rs                | 2 +-
 creusot/tests/should_succeed/mutex.rs               | 2 +-
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/creusot/tests/should_fail/bug/436_0.rs b/creusot/tests/should_fail/bug/436_0.rs
index 1fa6e050af..2fe0f54ff6 100644
--- a/creusot/tests/should_fail/bug/436_0.rs
+++ b/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 }
 }
diff --git a/creusot/tests/should_succeed/bug/545.rs b/creusot/tests/should_succeed/bug/545.rs
index 170dde32a4..5ac86e5ea2 100644
--- a/creusot/tests/should_succeed/bug/545.rs
+++ b/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);
 }
diff --git a/creusot/tests/should_succeed/bug/682.rs b/creusot/tests/should_succeed/bug/682.rs
index e26d997f37..722431d34c 100644
--- a/creusot/tests/should_succeed/bug/682.rs
+++ b/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;
diff --git a/creusot/tests/should_succeed/cell/01.rs b/creusot/tests/should_succeed/cell/01.rs
index c74245cea0..e973635fb6 100644
--- a/creusot/tests/should_succeed/cell/01.rs
+++ b/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
     }
 }
 
diff --git a/creusot/tests/should_succeed/list_reversal_lasso.rs b/creusot/tests/should_succeed/list_reversal_lasso.rs
index 52ee499a1e..a419909332 100644
--- a/creusot/tests/should_succeed/list_reversal_lasso.rs
+++ b/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 */
diff --git a/creusot/tests/should_succeed/mc91.rs b/creusot/tests/should_succeed/mc91.rs
index 5743ff8617..e85f56bc79 100644
--- a/creusot/tests/should_succeed/mc91.rs
+++ b/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
diff --git a/creusot/tests/should_succeed/mutex.rs b/creusot/tests/should_succeed/mutex.rs
index afea3c3895..296264f4a7 100644
--- a/creusot/tests/should_succeed/mutex.rs
+++ b/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
     }
 }