diff --git a/exercises/02_linear_search.rs b/exercises/02_linear_search.rs
index c384cdc6ae..84881a29ea 100644
--- a/exercises/02_linear_search.rs
+++ b/exercises/02_linear_search.rs
@@ -4,11 +4,11 @@ use creusot_contracts::*;
 // Prove the following:
 // 1. If we return Some(i) it is the first index containing `tgt`
 // 2. If we return None, then there are no indices containing `tgt`
-fn search<T: Ord>(v: &Vec<T>, tgt: &T) -> Option<usize> {
+fn search<T: Ord + DeepModel>(v: &[T], tgt: &T) -> Option<usize> {
     let mut i = 0;
 
     while i < v.len() {
-        if v[i] == tgt {
+        if v[i] == *tgt {
             return Some(i);
         }
 
diff --git a/exercises/04_all_zero.rs b/exercises/04_all_zero.rs
index 12b2aeef44..b89deb1cc0 100644
--- a/exercises/04_all_zero.rs
+++ b/exercises/04_all_zero.rs
@@ -6,9 +6,7 @@ use creusot_contracts::*;
 pub fn all_zero(v: &mut Vec<u32>) {
     let mut i = 0;
     let old_v = snapshot! { v };
-    // Until https://gitlab.inria.fr/why3/why3/-/merge_requests/667 is merged
-    // the following invariant is needed to allow Why3 to remember prophecies dont change
-    #[invariant(proph_const, ^v == ^old_v.inner())]
+
     while i < v.len() {
         v[i] = 0;
         i += 1;