about summary refs log tree commit diff homepage
path: root/lib/Basic/ConstructSolverChain.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Basic/ConstructSolverChain.cpp')
-rw-r--r--lib/Basic/ConstructSolverChain.cpp4
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;
 }