Reland "[analyzer] Harden safeguards for Z3 query times" by steakhal · Pull Request #97298 · llvm/llvm-project (original) (raw)

@llvm/pr-subscribers-clang-static-analyzer-1

@llvm/pr-subscribers-clang

Author: Balazs Benics (steakhal)

Changes

This is exactly as originally landed in #95129,
but now the minimal Z3 version was increased to meet this change in #96682.

https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

This patch is a functional change.
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

As a result of this patch, individual Z3 queries in refutation will be bound by 300ms. Every report equivalence class will be processed in at most 1 second.

The heuristic should have only really marginal observable impact - except for the cases when we had big report eqclasses with long-running (15s) Z3 queries, where previously CSA effectively halted. After this patch, CSA will tackle such extreme cases as well.

(cherry picked from commit eacc3b3)

Full diff: https://github.com/llvm/llvm-project/pull/97298.diff

6 Files Affected:

• (modified) clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def (+20)
• (modified) clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h (+34-8)
• (modified) clang/lib/StaticAnalyzer/Core/BugReporter.cpp (+10-2)
• (modified) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (+54-12)
• (modified) clang/test/Analysis/analyzer-config.c (+3)
• (modified) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (+100-16)

diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index f008c9c581d95..29aa6a3b8a16e 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -184,6 +184,26 @@ ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3", "constraint manager backend.", false)

+ANALYZER_OPTION(

• unsigned, Z3CrosscheckEQClassTimeoutThreshold,
• "crosscheck-with-z3-eqclass-timeout-threshold",
• "Set a timeout for bug report equivalence classes in milliseconds. "
• "If we exhaust this threshold, we will drop the bug report eqclass "
• "instead of doing more Z3 queries. Set 0 for no timeout.", 700)
• +ANALYZER_OPTION(
• unsigned, Z3CrosscheckTimeoutThreshold,
• "crosscheck-with-z3-timeout-threshold",
• "Set a timeout for individual Z3 queries in milliseconds. "
• "Set 0 for no timeout.", 300)
• +ANALYZER_OPTION(
• unsigned, Z3CrosscheckRLimitThreshold,
• "crosscheck-with-z3-rlimit-threshold",
• "Set the Z3 resource limit threshold. This sets a deterministic cutoff "
• "point for Z3 queries, as longer queries usually consume more resources. "
• "Set 0 for unlimited.", 400'000)
• ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile, "report-in-main-source-file", "Whether or not the diagnostic report should be always "

diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h index 9413fd739f607..439f37fa8604f 100644 --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h @@ -25,8 +25,11 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor { public: struct Z3Result { std::optional IsSAT = std::nullopt;

• unsigned Z3QueryTimeMilliseconds = 0;
• unsigned UsedRLimit = 0;

};

• explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);

• Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,

•                  const AnalyzerOptions &Opts);

  void Profile(llvm::FoldingSetNodeID &ID) const override;

@@ -44,21 +47,44 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor { /// Holds the constraints in a given path. ConstraintMap Constraints; Z3Result &Result;

• const AnalyzerOptions &Opts; };

/// The oracle will decide if a report should be accepted or rejected based on -/// the results of the Z3 solver. +/// the results of the Z3 solver and the statistics of the queries of a report +/// equivalenece class. class Z3CrosscheckOracle { public:

• explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
• enum Z3Decision {

• AcceptReport, // The report was SAT.
• RejectReport, // The report was UNSAT or UNDEF.

• AcceptReport, // The report was SAT.
• RejectReport, // The report was UNSAT or UNDEF.
• RejectEQClass, // The heuristic suggests to skip the current eqclass.

};

• /// Makes a decision for accepting or rejecting the report based on the
• /// result of the corresponding Z3 query.
• static Z3Decision
• interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Query);

• /// Updates the internal state with the new Z3Result and makes a decision how
• /// to proceed:
• /// - Accept the report if the Z3Result was SAT.
• /// - Suggest dropping the report equvalence class based on the accumulated
• /// statistics.
• /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF.
• ///
• /// Conditions for dropping the equivalence class:
• /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass.
• /// - Hit the 300ms query timeout in the report eqclass.
• /// - Hit the 400'000 rlimit in the report eqclass.
• ///
• /// All these thresholds are configurable via the analyzer options.
• ///
• /// Refer to
• /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to
• /// see why this heuristic was chosen.
• Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta);
• +private:
• const AnalyzerOptions &Opts;
• unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms };

} // namespace clang::ento diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp index c9a7fd0e035c2..e2002bfbe594a 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp @@ -89,6 +89,9 @@ STATISTIC(MaxValidBugClassSize,

STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3"); STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3"); +STATISTIC(NumTimesReportEQClassAborted,

•      "Number of times a report equivalence class was aborted by the Z3 "

•      "oracle heuristic");

STATISTIC(NumTimesReportEQClassWasExhausted, "Number of times all reports of an equivalence class was refuted");

@@ -2840,6 +2843,7 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R, std::optional PathDiagnosticBuilder::findValidReport( ArrayRef<PathSensitiveBugReport *> &bugReports, PathSensitiveBugReporter &Reporter) {

• Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());

  BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);

@@ -2871,16 +2875,20 @@ std::optional PathDiagnosticBuilder::findValidReport( // visitor and check again R->clearVisitors(); Z3CrosscheckVisitor::Z3Result CrosscheckResult;

•    R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult);

•    R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,

•                                       Reporter.getAnalyzerOptions());
  
     // We don't overwrite the notes inserted by other visitors because the
     // refutation manager does not add any new note to the path
     generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);

•    switch (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) {

•    switch (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
     case Z3CrosscheckOracle::RejectReport:
       ++NumTimesReportRefuted;
       R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
       continue;

•    case Z3CrosscheckOracle::RejectEQClass:

•      ++NumTimesReportEQClassAborted;

•      return {};
     case Z3CrosscheckOracle::AcceptReport:
       ++NumTimesReportPassesZ3;
       break;

diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index a7db44ef8ea30..739db951b3e18 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -12,26 +12,37 @@ //===----------------------------------------------------------------------===//

#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" +#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" #include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/SMTAPI.h" +#include "llvm/Support/Timer.h"

#define DEBUG_TYPE "Z3CrosscheckOracle"

STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done"); STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out"); +STATISTIC(NumTimesZ3ExhaustedRLimit,

•      "Number of times Z3 query exhausted the rlimit");

+STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,

•      "Number of times report equivalenece class was cut because it spent "

•      "too much time in Z3");

STATISTIC(NumTimesZ3QueryAcceptsReport, "Number of Z3 queries accepting a report"); STATISTIC(NumTimesZ3QueryRejectReport, "Number of Z3 queries rejecting a report"); +STATISTIC(NumTimesZ3QueryRejectEQClass,

•      "Number of times rejecting an report equivalenece class");

using namespace clang; using namespace ento;

-Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)

• : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}

+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,

•                                     const AnalyzerOptions &Opts)

• : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),

•  Opts(Opts) {}

void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, @@ -41,8 +52,12 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,

// Create a refutation manager llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();

• RefutationSolver->setBoolParam("model", true); // Enable model finding
• RefutationSolver->setUnsignedParam("timeout", 15000); // ms

• if (Opts.Z3CrosscheckRLimitThreshold)
• RefutationSolver->setUnsignedParam("rlimit",

•                                   Opts.Z3CrosscheckRLimitThreshold);

• if (Opts.Z3CrosscheckTimeoutThreshold)
• RefutationSolver->setUnsignedParam("timeout",

•                                   Opts.Z3CrosscheckTimeoutThreshold); // ms

  ASTContext &Ctx = BRC.getASTContext();

@@ -63,8 +78,15 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, }

// And check for satisfiability

• llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/Start=/true); std::optional IsSAT = RefutationSolver->check();

• Result = Z3Result{IsSAT};

• llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/Start=/false);
• Diff -= Start;
• Result = Z3Result{

•  IsSAT,

•  static_cast<unsigned>(Diff.getWallTime() * 1000),

•  RefutationSolver->getStatistics()->getUnsigned("rlimit count"),

• }; }

void Z3CrosscheckVisitor::addConstraints( @@ -101,18 +123,38 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const { Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult( const Z3CrosscheckVisitor::Z3Result &Query) { ++NumZ3QueriesDone;

• AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;

• if (!Query.IsSAT.has_value()) {
• // For backward compatibility, let's accept the first timeout.
• ++NumTimesZ3TimedOut;

• if (Query.IsSAT && Query.IsSAT.value()) {
• ++NumTimesZ3QueryAcceptsReport; return AcceptReport; }

• if (Query.IsSAT.value()) {
• ++NumTimesZ3QueryAcceptsReport;
• return AcceptReport; // sat

• // Suggest cutting the EQClass if certain heuristics trigger.
• if (Opts.Z3CrosscheckTimeoutThreshold &&

•  Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {

• ++NumTimesZ3TimedOut;
• ++NumTimesZ3QueryRejectEQClass;
• return RejectEQClass;
• }
• if (Opts.Z3CrosscheckRLimitThreshold &&

•  Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {

• ++NumTimesZ3ExhaustedRLimit;
• ++NumTimesZ3QueryRejectEQClass;
• return RejectEQClass;
• }
• if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&

•  AccumulatedZ3QueryTimeInEqClass >

•      Opts.Z3CrosscheckEQClassTimeoutThreshold) {

• ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
• ++NumTimesZ3QueryRejectEQClass;
• return RejectEQClass;

}

• // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
• // then reject the report. ++NumTimesZ3QueryRejectReport;

• return RejectReport; // unsat

• return RejectReport; } diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c index fda920fa3951e..2a4c40005a4dc 100644 --- a/clang/test/Analysis/analyzer-config.c +++ b/clang/test/Analysis/analyzer-config.c @@ -43,6 +43,9 @@ // CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals // CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false // CHECK-NEXT: crosscheck-with-z3 = false +// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700 +// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 400000 +// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300 // CHECK-NEXT: ctu-dir = "" // CHECK-NEXT: ctu-import-cpp-threshold = 8 // CHECK-NEXT: ctu-import-threshold = 24 diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp index efad4dd3f03b9..ef07e47ee911b 100644 --- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp +++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp @@ -6,6 +6,7 @@ // //===----------------------------------------------------------------------===//

+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" #include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" #include "gtest/gtest.h"

@@ -17,43 +18,126 @@ using Z3Decision = Z3CrosscheckOracle::Z3Decision;

static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport; static constexpr Z3Decision RejectReport = Z3Decision::RejectReport; +static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass;

static constexpr std::optional SAT = true; static constexpr std::optional UNSAT = false; static constexpr std::optional UNDEF = std::nullopt;

+static unsigned operator""_ms(unsigned long long ms) { return ms; } +static unsigned operator""_step(unsigned long long rlimit) { return rlimit; } + +static const AnalyzerOptions DefaultOpts = [] {

• AnalyzerOptions Config; +#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC, \

•                                         SHALLOW_VAL, DEEP_VAL)            \

• ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL) +#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL) \
• Config.NAME = DEFAULT_VAL; +#include "clang/StaticAnalyzer/Core/AnalyzerOptions.def"
• // Remember to update the tests in this file when these values change.
• // Also update the doc comment of interpretQueryResult.
• assert(Config.Z3CrosscheckRLimitThreshold == 400'000);
• assert(Config.Z3CrosscheckTimeoutThreshold == 300_ms);
• // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly
• // overshoots until it realizes that it overshoot and needs to back off.
• // Consequently, the measured timeout should be fairly close to the threshold.
• // Same reasoning applies to the rlimit too.
• return Config; +}();
• namespace {

-struct Z3CrosscheckOracleTest : public testing::Test {

• Z3Decision interpretQueryResult(const Z3Result &Result) const {
• return Z3CrosscheckOracle::interpretQueryResult(Result);

+class Z3CrosscheckOracleTest : public testing::Test { +public:

• Z3Decision interpretQueryResult(const Z3Result &Result) {
• return Oracle.interpretQueryResult(Result);

} + +private:

• Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts); };

TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {

• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));

• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); }

TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {

• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));

• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); +}
• +TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
• // Even if it times out, if it is SAT, we should accept it.
• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step})); }

-TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {

• ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF})); +TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {

• ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step})); }

-TEST_F(Z3CrosscheckOracleTest, AcceptsTimeout) {

• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
• ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF})); +TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) {

• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step})); }

TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) {

• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));

• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); +}
• +// Testing cut heuristics: +// =======================
• +TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
• // Simulate long queries, that barely doesn't trigger the timeout.
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
• ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step})); +}
• +TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
• // Simulate long queries, that barely doesn't trigger the timeout.
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step})); +}
• +TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
• // Simulate quick, but many queries: 35 quick UNSAT queries.
• // 35*20ms = 700ms, which is equal to the 700ms threshold.
• for (int i = 0; i < 35; ++i) {
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
• }
• // Do one more to trigger the heuristic.
• ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step})); +}
• +TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
• // Simulate quick, but many queries: 35 quick UNSAT queries.
• // 35*20ms = 700ms, which is equal to the 700ms threshold.
• for (int i = 0; i < 35; ++i) {
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
• }
• // Do one more to trigger the heuristic, but given this was SAT, we still
• // accept the query.
• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step})); +}
• +TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step})); +}
• +TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
• ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step})); }

} // namespace