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/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index b48c5cb0..2df87d51 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -62,6 +62,10 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
     llvm::errs() << "Logging all queries in .smt2 format to "
                  << querySMT2LogPath.c_str() << "\n";
   }
+  if (DebugCrossCheckCoreSolverWith != NO_SOLVER) {
+    Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith);
+    solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver);
+  }
 
   return solver;
 }