Add ``-debug-cross-check-core-solver`` option to allow cross-checking

with another solver. For example the core solver can be STP and the
cross checking solver can be Z3.

Unfortunately a few fragile tests don't pass when actually using this
option.

1 files changed, 4 insertions, 0 deletions

diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 66328f30..783047f8 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -83,11 +83,15 @@ Solver *createCoreSolver(CoreSolverType cst) {
     return createDummySolver();
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
+    llvm::errs() << "Using Z3 solver backend\n";
     return new Z3Solver();
 #else
     llvm::errs() << "Not compiled with Z3 support\n";
     return NULL;
 #endif
+  case NO_SOLVER:
+    llvm::errs() << "Invalid solver\n";
+    return NULL;
   default:
     llvm_unreachable("Unsupported CoreSolverType");
   }