Remove redundant invariant

viperproject · Jan 11, 2024 · 1060d44 · 1060d44
1 parent 216e5db
commit 1060d44
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs b/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs
@@ -34,7 +34,6 @@ pub fn bisect<T: Function>(f: &T, target: i32) -> Option<usize> {
     let mut low = 0;
     let mut high = f.domain_size();
     while low < high {
-        body_invariant!(f.invariant());
         body_invariant!(high <= f.domain_size());
         body_invariant!(forall(|x: usize|
             (x < low || high <= x) && x < f.domain_size() ==> f.eval(x) != target