[llvm-branch-commits] [analyzer] Harden safeguards for Z3 query times (PR #95129)

[Donát Nagy via llvm-branch-commits]

================
@@ -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