Try disabling function unfolding triggers.

Author: vakaras

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::*;