2 files changed, 7 insertions, 0 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index e55c4550..82cb01b2 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -82,6 +82,10 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     llvm::cl::CommaSeparated
 );
 
+llvm::cl::opt<bool>
+    UseAssignmentValidatingSolver("debug-assignment-validating-solver",
+                                  llvm::cl::init(false));
+
 #ifdef ENABLE_METASMT
 
 #ifdef METASMT_DEFAULT_BACKEND_IS_BTOR
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 68e1b08b..d00fcec1 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -37,6 +37,9 @@ Solver *constructSolverChain(Solver *coreSolver,
                  baseSolverQuerySMT2LogPath.c_str());
   }
 
+  if (UseAssignmentValidatingSolver)
+    solver = createAssignmentValidatingSolver(solver);
+
   if (UseFastCexSolver)
     solver = createFastCexSolver(solver);