From fdf48117bfd9efe310d7a8d64226b345ca1e30e8 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Fri, 8 Dec 2023 20:37:10 +0100 Subject: [PATCH] Disable more complete exhale. --- .../pass/rosetta/Binary_search/artefact_Binary_search_shared.rs | 2 ++ .../artefact_Binary_search_shared_fixed_termination.rs | 2 ++ .../artefact_Binary_search_shared_monomorphised.rs | 2 ++ ...fact_Binary_search_shared_monomorphised_fixed_termination.rs | 2 ++ 4 files changed, 8 insertions(+) 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.