From d34a946acb7f5155ee62f1bdc95ae7ef7b848e49 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 11 Apr 2016 08:19:02 -0500
Subject: 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.
---
 lib/Solver/CoreSolver.cpp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/Solver')

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");
   }
-- 
cgit 1.4.1