Searched refs:RefutationSolver (Results 1 – 1 of 1) sorted by relevance
| /freebsd/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/ |
| H A D | Z3CrosscheckVisitor.cpp | 64 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); in finalizeVisitor() local
66 RefutationSolver->setUnsignedParam("rlimit", in finalizeVisitor()
69 RefutationSolver->setUnsignedParam("timeout", in finalizeVisitor()
79 RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), in finalizeVisitor()
82 SMTConstraints = RefutationSolver->mkOr( in finalizeVisitor()
83 SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, in finalizeVisitor()
87 RefutationSolver->addConstraint(SMTConstraints); in finalizeVisitor()
110 Result = AttemptOnce(RefutationSolver); in finalizeVisitor()
|