diff options
| author | Julian Büning <julian.buening@rwth-aachen.de> | 2022-01-05 22:43:23 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2022-03-17 22:59:26 +0000 |
| commit | 1b51cf5ecde7ca9e6646d481b0d757dd31b06da8 (patch) | |
| tree | af3dbec1ca297e4eacc736ba6bb6b012c2a2a8c3 /lib/Solver | |
| parent | fcb5641d29b2e22bbd4034e51a1fe675b69bbf81 (diff) | |
| download | klee-1b51cf5ecde7ca9e6646d481b0d757dd31b06da8.tar.gz | |
remove obsolete KLEE_LLVM legacy defines
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/SolverCmdLine.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index 7dd8f041..d91261dc 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -104,8 +104,7 @@ cl::bits<QueryLoggingSolverType> QueryLoggingOptions( "All queries reaching the solver in .kquery (KQuery) format"), clEnumValN( SOLVER_SMTLIB, "solver:smt2", - "All queries reaching the solver in .smt2 (SMT-LIBv2) format") - KLEE_LLVM_CL_VAL_END), + "All queries reaching the solver in .smt2 (SMT-LIBv2) format")), cl::CommaSeparated, cl::cat(SolvingCat)); cl::opt<bool> UseAssignmentValidatingSolver( @@ -158,8 +157,7 @@ MetaSMTBackend("metasmt-backend", clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"), - clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2") - KLEE_LLVM_CL_VAL_END), + clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2")), cl::init(METASMT_DEFAULT_BACKEND), cl::cat(SolvingCat)); @@ -195,8 +193,7 @@ cl::opt<CoreSolverType> CoreSolverToUse( clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), - clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR) - KLEE_LLVM_CL_VAL_END), + clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)), cl::init(DEFAULT_CORE_SOLVER), cl::cat(SolvingCat)); cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith( @@ -207,8 +204,7 @@ cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith( clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3"), - clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)") - KLEE_LLVM_CL_VAL_END), + clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")), cl::init(NO_SOLVER), cl::cat(SolvingCat)); } // namespace klee |