Disable more complete exhale.

viperproject · Dec 8, 2023 · fdf4811 · fdf4811
1 parent 9567ddd
commit fdf4811
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 0 deletions.
diff --git a/...i-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs b/...i-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/...fy_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs b/...fy_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/...verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs b/...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/...ss/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs b/...ss/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.