[llvm-branch-commits] [clang] bbcee74 - Revert "[analyzer] Harden safeguards for Z3 query times"
via llvm-branch-commits
llvm-branch-commits at lists.llvm.org
Tue Jun 18 05:50:03 PDT 2024
Author: Balazs Benics
Date: 2024-06-18T14:50:00+02:00
New Revision: bbcee744465c72b8000321defd85ed3daa290502
URL: https://github.com/llvm/llvm-project/commit/bbcee744465c72b8000321defd85ed3daa290502
DIFF: https://github.com/llvm/llvm-project/commit/bbcee744465c72b8000321defd85ed3daa290502.diff
LOG: Revert "[analyzer] Harden safeguards for Z3 query times"
This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a.
Added:
Modified:
clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
clang/lib/StaticAnalyzer/Core/BugReporter.cpp
clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
clang/test/Analysis/analyzer-config.c
clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
index 29aa6a3b8a16e..f008c9c581d95 100644
--- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
+++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
@@ -184,26 +184,6 @@ 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 439f37fa8604f..9413fd739f607 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
@@ -25,11 +25,8 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor {
public:
struct Z3Result {
std::optional<bool> IsSAT = std::nullopt;
- unsigned Z3QueryTimeMilliseconds = 0;
- unsigned UsedRLimit = 0;
};
- Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
- const AnalyzerOptions &Opts);
+ explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
void Profile(llvm::FoldingSetNodeID &ID) const override;
@@ -47,44 +44,21 @@ 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 and the statistics of the queries of a report
-/// equivalenece class.
+/// the results of the Z3 solver.
class Z3CrosscheckOracle {
public:
- explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
-
enum Z3Decision {
- AcceptReport, // The report was SAT.
- RejectReport, // The report was UNSAT or UNDEF.
- RejectEQClass, // The heuristic suggests to skip the current eqclass.
+ AcceptReport, // The report was SAT.
+ RejectReport, // The report was UNSAT or UNDEF.
};
- /// 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
+ /// 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);
};
} // namespace clang::ento
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index e2002bfbe594a..c9a7fd0e035c2 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -89,9 +89,6 @@ 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");
@@ -2843,7 +2840,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
ArrayRef<PathSensitiveBugReport *> &bugReports,
PathSensitiveBugReporter &Reporter) {
- Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
@@ -2875,20 +2871,16 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
// visitor and check again
R->clearVisitors();
Z3CrosscheckVisitor::Z3Result CrosscheckResult;
- R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
- Reporter.getAnalyzerOptions());
+ R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult);
// 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 (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
+ switch (Z3CrosscheckOracle::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 739db951b3e18..a7db44ef8ea30 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
@@ -12,37 +12,26 @@
//===----------------------------------------------------------------------===//
#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,
- const AnalyzerOptions &Opts)
- : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
- Opts(Opts) {}
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
+ : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
const ExplodedNode *EndPathNode,
@@ -52,12 +41,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
// Create a refutation manager
llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
- if (Opts.Z3CrosscheckRLimitThreshold)
- RefutationSolver->setUnsignedParam("rlimit",
- Opts.Z3CrosscheckRLimitThreshold);
- if (Opts.Z3CrosscheckTimeoutThreshold)
- RefutationSolver->setUnsignedParam("timeout",
- Opts.Z3CrosscheckTimeoutThreshold); // ms
+ RefutationSolver->setBoolParam("model", true); // Enable model finding
+ RefutationSolver->setUnsignedParam("timeout", 15000); // ms
ASTContext &Ctx = BRC.getASTContext();
@@ -78,15 +63,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
}
// 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"),
- };
+ Result = Z3Result{IsSAT};
}
void Z3CrosscheckVisitor::addConstraints(
@@ -123,38 +101,18 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
const Z3CrosscheckVisitor::Z3Result &Query) {
++NumZ3QueriesDone;
- AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
- if (Query.IsSAT && Query.IsSAT.value()) {
- ++NumTimesZ3QueryAcceptsReport;
- return AcceptReport;
- }
-
- // Suggest cutting the EQClass if certain heuristics trigger.
- if (Opts.Z3CrosscheckTimeoutThreshold &&
- Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
+ if (!Query.IsSAT.has_value()) {
+ // For backward compatibility, let's accept the first timeout.
++NumTimesZ3TimedOut;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
- }
-
- if (Opts.Z3CrosscheckRLimitThreshold &&
- Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
- ++NumTimesZ3ExhaustedRLimit;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
+ return AcceptReport;
}
- if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
- AccumulatedZ3QueryTimeInEqClass >
- Opts.Z3CrosscheckEQClassTimeoutThreshold) {
- ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
+ if (Query.IsSAT.value()) {
+ ++NumTimesZ3QueryAcceptsReport;
+ return AcceptReport; // sat
}
- // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
- // then reject the report.
++NumTimesZ3QueryRejectReport;
- return RejectReport;
+ return RejectReport; // unsat
}
diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c
index 2a4c40005a4dc..fda920fa3951e 100644
--- a/clang/test/Analysis/analyzer-config.c
+++ b/clang/test/Analysis/analyzer-config.c
@@ -43,9 +43,6 @@
// 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 ef07e47ee911b..efad4dd3f03b9 100644
--- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
+++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
@@ -6,7 +6,6 @@
//
//===----------------------------------------------------------------------===//
-#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "gtest/gtest.h"
@@ -18,126 +17,43 @@ 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<bool> SAT = true;
static constexpr std::optional<bool> UNSAT = false;
static constexpr std::optional<bool> 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 {
-class Z3CrosscheckOracleTest : public testing::Test {
-public:
- Z3Decision interpretQueryResult(const Z3Result &Result) {
- return Oracle.interpretQueryResult(Result);
+struct Z3CrosscheckOracleTest : public testing::Test {
+ Z3Decision interpretQueryResult(const Z3Result &Result) const {
+ return Z3CrosscheckOracle::interpretQueryResult(Result);
}
-
-private:
- Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
};
TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
}
TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
- 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}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
}
-TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
+ 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, AcceptsTimeout) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
}
TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) {
- 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}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
}
} // namespace
More information about the llvm-branch-commits
mailing list