diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs
index be9972060a9..a0465881401 100644
--- a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs
@@ -1,3 +1,5 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
 //! An adaptation of the example from
 //! https://rosettacode.org/wiki/Binary_search#Rust
 //!
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs
index dbb2d146e01..8916a3d83a1 100644
--- a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs
@@ -1,3 +1,5 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
 //! A copy of `artefact_Binary_search_shared.rs` with fixed non-termination bug and manually
 //! encoded termination check.
 
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs
index 5192f1172ca..65962859a4e 100644
--- a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs
@@ -1,3 +1,5 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
 //! An adaptation of the example from
 //! https://rosettacode.org/wiki/Binary_search#Rust
 //!
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs
index c9d7a4d4b9c..b13b9852458 100644
--- a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs
@@ -1,3 +1,5 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
 //! A copy of `artefact_Binary_search_shared.rs` with fixed non-termination bug and manually
 //! encoded termination check.