Searched refs:RefutationSolver (Results 1 – 1 of 1) sorted by relevance
| /freebsd/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/ |
| H A D | Z3CrosscheckVisitor.cpp | 54 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); in finalizeVisitor() local
56 RefutationSolver->setUnsignedParam("rlimit", in finalizeVisitor()
59 RefutationSolver->setUnsignedParam("timeout", in finalizeVisitor()
69 RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), in finalizeVisitor()
72 SMTConstraints = RefutationSolver->mkOr( in finalizeVisitor()
73 SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, in finalizeVisitor()
77 RefutationSolver->addConstraint(SMTConstraints); in finalizeVisitor()
82 std::optional<bool> IsSAT = RefutationSolver->check(); in finalizeVisitor()
88 RefutationSolver->getStatistics()->getUnsigned("rlimit count"), in finalizeVisitor()
|