From e81f5ceed580d4d267e3c857b47637d6bd065499 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Jan 2016 12:00:25 +0000 Subject: Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles... --- unittests/Solver/SolverTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'unittests/Solver') diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 16bd3ce4..38e055cd 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -10,6 +10,7 @@ #include #include "gtest/gtest.h" +#include "klee/CommandLine.h" #include "klee/Constraints.h" #include "klee/Expr.h" #include "klee/Solver.h" @@ -127,8 +128,7 @@ void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true, } TEST(SolverTest, Evaluation) { - STPSolver *stpSolver = new STPSolver(true); - Solver *solver = stpSolver; + Solver *solver = klee::createCoreSolver(CoreSolverToUse); solver = createCexCachingSolver(solver); solver = createCachingSolver(solver); -- cgit 1.4.1