Author: Balazs Benics Date: 2024-07-01T17:22:24+02:00 New Revision: ae570d82e8c021f45209830db8c9c7bb79bed394
URL: https://github.com/llvm/llvm-project/commit/ae570d82e8c021f45209830db8c9c7bb79bed394 DIFF: https://github.com/llvm/llvm-project/commit/ae570d82e8c021f45209830db8c9c7bb79bed394.diff LOG: Reland "[analyzer] Harden safeguards for Z3 query times" (#97298) 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 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 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<bool> 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> PathDiagnosticBuilder::findValidReport( ArrayRef<PathSensitiveBugReport *> &bugReports, PathSensitiveBugReporter &Reporter) { + Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions()); BugPathGetter BugGraph(&Reporter.getGraph(), bugReports); @@ -2871,16 +2875,20 @@ std::optional<PathDiagnosticBuilder> 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<bool> 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<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 { -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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
