Try disabling function unfolding triggers.

prusti-server/src/verification_request.rs

@@ -42,6 +42,9 @@ impl ViperBackendConfig {
                 if config::use_more_complete_exhale() {
                     verifier_args.push("--enableMoreCompleteExhale".to_string());
                 }
+                if config::disable_function_unfold_trigger() {
+                    verifier_args.push("--disableFunctionUnfoldTrigger".to_string());
+                }
                 if config::counterexample() {
                     verifier_args.push("--counterexample".to_string());
                     verifier_args.push("mapped".to_string());

prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(box_patterns, box_syntax)]
 use prusti_contracts::*;
 

prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(nll)]
 #![feature(box_patterns)]
 #![feature(box_syntax)]

prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 //! Issue #39 "Suspicious `_old_old_1` variable name"
 
 #![feature(nll)]

prusti-tests/tests/verify/pass/larger/first-final.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(box_patterns)]
 
 //! An adaptation of the example from

prusti-tests/tests/verify/pass/magic-wands/from_nth.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(box_patterns)]
 
 use prusti_contracts::*;

prusti-tests/tests/verify/pass/paper-examples/routes.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(box_syntax, box_patterns)]
 
 use prusti_contracts::*;

prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(nll)]
 #![feature(box_patterns)]
 #![feature(box_syntax)]

prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(nll)]
 #![feature(box_patterns)]
 #![feature(box_syntax)]

prusti-tests/tests/verify/pass/quick/routes.rs

@@ -1,3 +1,5 @@
+// compile-flags: -Pdisable_function_unfold_trigger=false
+
 #![feature(box_syntax, box_patterns)]
 
 use prusti_contracts::*;

prusti-utils/src/config.rs

@@ -102,6 +102,7 @@ lazy_static::lazy_static! {
         settings.set_default("assert_timeout", 10_000).unwrap();
         settings.set_default("smt_qi_eager_threshold", 1000).unwrap();
         settings.set_default("use_more_complete_exhale", true).unwrap();
+        settings.set_default("disable_function_unfold_trigger", true).unwrap();
         settings.set_default("skip_unsupported_features", false).unwrap();
         settings.set_default("internal_errors_as_warnings", false).unwrap();
         settings.set_default("allow_unreachable_unsupported_code", false).unwrap();
@@ -510,6 +511,13 @@ pub fn use_more_complete_exhale() -> bool {
     read_setting("use_more_complete_exhale")
 }
 
+/// When enabled, disables unfolding of functions together with unfolding
+/// predicates. Equivalent to the verifier command-line argument
+/// `--disableFunctionUnfoldTrigger`.
+pub fn disable_function_unfold_trigger() -> bool {
+    read_setting("disable_function_unfold_trigger")
+}
+
 /// When enabled, prints the items collected for verification.
 pub fn print_collected_verification_items() -> bool {
     read_setting("print_collected_verification_items")

viper-toolchain

@@ -1 +1 @@
-v-2022-10-31-1114
+v-2022-11-04-0724