From d55e90e1e708414617c490bd99a870b999a011b0 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 15 Aug 2010 10:55:18 +0000
Subject: [PATCH] Extra tests for inactive by-default code

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@986 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/BitBlaster.cpp | 28 +++++++++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 553d9a7..718008d 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -98,7 +98,7 @@ bool BitBlaster<BBNode,BBNodeManagerT>::update(const ASTNode&n, const int i, sim
 {
         if (b->isFixed(i) && (!(bb == BBTrue || bb == BBFalse)))
         {
-                //We have a fixed bit, but the bitblasted values aren't constant true or false.
+          //We have a fixed bit, but the bitblasted values aren't constant true or false.
             if (conjoin_to_top && (fixedFromBottom.find(n) == fixedFromBottom.end()))
             {
               if (b->getValue(i))
@@ -193,9 +193,27 @@ void BitBlaster<BBNode,BBNodeManagerT>::updateTerm(const ASTNode&n, BBNodeVec& b
                 cb->propagate();
                 //cerr << "##!!" << endl;
         }
+
+        if (!cb->isUnsatisfiable())
+          for (int i = 0; i < (int) bb.size(); i++)
+          {
+            if (b->isFixed(i) && b->getValue(i))
+              assert(bb[i] == BBTrue);
+
+            if (b->isFixed(i) && !b->getValue(i))
+              assert(bb[i] == BBFalse);
+
+            if (bb[i] == BBFalse)
+              assert( b->isFixed(i) && !b->getValue(i));
+
+            if (bb[i] == BBTrue)
+              assert( b->isFixed(i) && b->getValue(i));
+          }
 }
 
 
+
+
 template <class BBNode, class BBNodeManagerT>
 const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, BBNodeSet& support) {
         typename BBNodeVecMap::iterator it = BBTermMemo.find(term);
@@ -399,8 +417,9 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
 		assert(BVTypeCheck(term));
 		assert(term.Degree() == 2);
 
-		const BBNodeVec& mpcd1 = BBTerm(term[0], support);
-		const BBNodeVec& mpcd2 = BBTerm(term[1], support);
+               const BBNodeVec& mpcd1 = BBTerm(term[0], support);
+               const BBNodeVec& mpcd2 = BBTerm(term[1], support);
+
 		assert(mpcd1.size() == mpcd2.size());
 		result = BBMult(mpcd1, mpcd2, support,term);
 		break;
@@ -1247,6 +1266,9 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::mult_normal(const BBNodeVec& x,
     if (cb == NULL)
       return;
 
+    if (cb->isUnsatisfiable())
+      return;
+
     if (cb->fixedMap->map->find(n) != cb->fixedMap->map->end())
       {
         FixedBits* b = cb->fixedMap->map->find(n)->second;
-- 
2.47.3