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...

1 files changed, 2 insertions, 2 deletions

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 <iostream>
 #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);