do not attempt a recommends check if the primary query/ies timed out (f…

…ixes #1412) it is confusing to the user, and it may pollute the profiler information
verus-lang · Jan 27, 2025 · 8d7ba77 · 8d7ba77
1 parent a8a3ce3
commit 8d7ba77
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 32 deletions.
diff --git a/source/rust_verify/example/playground.rs b/source/rust_verify/example/playground.rs
@@ -3,39 +3,39 @@ use builtin_macros::*;
 
 verus! {
 
-#[derive(PartialEq, Eq, Structural)]
-struct S<A> {
-    a: A,
-    b: bool,
-}
-
-fn add1(a: &mut u32)
-    requires
-        *old(a) < 10,
-    ensures
-        *a == *old(a) + 1,
-{
-    *a = *a + 1;
-}
-
-fn foo(s: S<u32>) {
-    // let mut s = s;
-    let mut s = S { a: 5, b: false };
-    add1(&mut s.a);
-    assert(s.a == 6);
-    assert(s.b == false);
-    assert(s == S { a: 6u32, b: false });
-}
+// #[derive(PartialEq, Eq, Structural)]
+// struct S<A> {
+//     a: A,
+//     b: bool,
+// }
+// 
+// fn add1(a: &mut u32)
+//     requires
+//         *old(a) < 10,
+//     ensures
+//         *a == *old(a) + 1,
+// {
+//     *a = *a + 1;
+// }
+// 
+// fn foo(s: S<u32>) {
+//     // let mut s = s;
+//     let mut s = S { a: 5, b: false };
+//     add1(&mut s.a);
+//     assert(s.a == 6);
+//     assert(s.b == false);
+//     assert(s == S { a: 6u32, b: false });
+// }
 
 // The following causes a trigger loop (useful for testing rlimit-related features):
 //
-// spec fn f(x: nat, y: nat) -> bool;
-//
-// proof fn goodbye_z3()
-//     requires forall|x: nat, y: nat| f(x + 1, 2 * y) && f(2 * x, y + x) || f(y, x) ==> (#[trigger] f(x, y)),
-//     ensures forall|x: nat, y: nat| x > 2318 && y < 100 ==> f(x, y),
-// {
-// }
+spec fn f(x: nat, y: nat) -> bool;
+
+proof fn goodbye_z3()
+    requires forall|x: nat, y: nat| f(x + 1, 2 * y) && f(2 * x, y + x) || f(y, x) ==> (#[trigger] f(x, y)),
+    ensures forall|x: nat, y: nat| x > 2318 && y < 100 ==> f(x, y),
+{
+}
 fn main() {
 }
 

diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs
@@ -1744,7 +1744,9 @@ impl Verifier {
                         }
 
                         if matches!(query_op, QueryOp::Body(Style::Normal)) {
-                            if (any_invalid && !self.args.no_auto_recommends_check)
+                            if (any_invalid
+                                && !self.args.no_auto_recommends_check
+                                && !any_timed_out)
                                 || function.x.attrs.check_recommends
                             {
                                 function_opgen.retry_with_recommends(&op, any_invalid)?;
@@ -1772,7 +1774,9 @@ impl Verifier {
                         }
 
                         if matches!(query_op, QueryOp::SpecTermination) {
-                            if (any_invalid && !self.args.no_auto_recommends_check)
+                            if (any_invalid
+                                && !self.args.no_auto_recommends_check
+                                && !any_timed_out)
                                 || function.x.attrs.check_recommends
                             {
                                 // Do recommends-checking for the body of the function.