================
@@ -101,18 +123,37 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID
&ID) const {
Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
const Z3CrosscheckVisitor::Z3Result &Query) {
++NumZ3QueriesDone;
+ ++NumZ3QueriesDoneInEqClass;
+ AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
- if (!Query.IsSAT.has_value()) {
- // For backward compatibility, let's accept the first timeout.
+ if (Query.IsSAT && Query.IsSAT.value()) {
+ ++NumTimesZ3QueryAcceptsReport;
+ return AcceptReport; // sat
----------------
NagyDonat wrote:
```suggestion
return AcceptReport;
```
This old comment doesn't add anything + the "unset" on the other branch was
slightly incorrect.
https://github.com/llvm/llvm-project/pull/95129
_______________________________________________
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
