From 2ade23b118bf07148de7e2cc55ac5e550335e383 Mon Sep 17 00:00:00 2001
From: Federico Poli <fpoli@users.noreply.github.com>
Date: Thu, 11 Jan 2024 12:31:40 +0100
Subject: [PATCH] Remove redundant invariant (#1487)

---
 prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs b/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs
index 9ad25f16cf0..eb185954ff9 100644
--- 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