================
@@ -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) {
----------------
NagyDonat wrote:
```suggestion
for (unsigned i = 0; i <= Opts.Z3CrosscheckRetriesOnTimeout; i++) {
```
It is more readable to stick to the common idiomatic 0-based loop format.
Also, technically the 1-based loop is buggy if the user specifies `UINT_MAX` as
the `Z3CrosscheckRetriesOnTimeout` value (which is a bad idea but not
completely implausible -- somebody might think it's a good idea to specify "I
want to do infinite retries") and the addition overflows.
https://github.com/llvm/llvm-project/pull/120239
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
