[clang] [analyzer] Retry UNDEF Z3 queries at most "crosscheck-with-z3-retries-on-timeout" times (PR #120239)

[Balazs Benics via cfe-commits]

================
@@ -77,16 +80,33 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
     RefutationSolver->addConstraint(SMTConstraints);
   }
 
-  // And check for satisfiability
-  llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true);
-  std::optional<bool> IsSAT = RefutationSolver->check();
-  llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false);
-  Diff -= Start;
-  Result = Z3Result{
-      IsSAT,
-      static_cast<unsigned>(Diff.getWallTime() * 1000),
-      RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
+  auto GetUsedRLimit = [](const llvm::SMTSolverRef &Solver) {
+    return Solver->getStatistics()->getUnsigned("rlimit count");
+  };
+
+  auto AttemptOnce = [&](const llvm::SMTSolverRef &Solver) -> Z3Result {
+    constexpr auto getCurrentTime = llvm::TimeRecord::getCurrentTime;
+    unsigned InitialRLimit = GetUsedRLimit(Solver);
+    double Start = getCurrentTime(/*Start=*/true).getWallTime();
+    std::optional<bool> IsSAT = Solver->check();
+    double End = getCurrentTime(/*Start=*/false).getWallTime();
+    return {
+        IsSAT,
+        static_cast<unsigned>((End - Start) * 1000),
+        GetUsedRLimit(Solver) - InitialRLimit,
+    };
   };
+
+  // And check for satisfiability
+  unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max();
+  unsigned NumRetries = Opts.Z3CrosscheckRetriesOnTimeout;
+  for (unsigned Attempt = 1; Attempt <= 1 + NumRetries; ++Attempt) {
----------------
steakhal wrote:

I'm fine either way. I accepted the suggestion in https://github.com/llvm/llvm-project/pull/120239/commits/7dc6f3162a0ce5c3168766e01dc10638d6b12c7f.

https://github.com/llvm/llvm-project/pull/120239