From 4530447c21353b5596b66a9fbb642409cda56f73 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 15 Sep 2016 12:09:23 +0100
Subject: 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.
---
 lib/Basic/ConstructSolverChain.cpp | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib/Basic/ConstructSolverChain.cpp')

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