Add `AssignmentValidatingSolver`. It's purpose is to check any computed

assignments against the corresponding `Query` object and check the
assignment evaluates correctly.

This can be switched on using `-debug-assignment-validating-solver`
on the command line.

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);