diff --git a/sources b/sources
index ae8501f..7ed9a01 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-78da1267ffbbbd8a87a02bac476f6642  stp-0.1.tar.xz
+e23ce5a6ef6cc34ce289c2d4eb948efe  stp-0.1.tar.xz
diff --git a/stp-warning.patch b/stp-warning.patch
index 5884d43..3133ca8 100644
--- a/stp-warning.patch
+++ b/stp-warning.patch
@@ -1,5 +1,5 @@
 --- ./src/simplifier/UseITEContext.h.orig	2011-04-07 07:38:52.000000000 -0600
-+++ ./src/simplifier/UseITEContext.h	2011-12-13 13:08:15.892474675 -0700
++++ ./src/simplifier/UseITEContext.h	2012-01-10 16:05:21.201610452 -0700
 @@ -27,7 +27,7 @@ namespace BEEV
        if (n.GetKind() == NOT && n[0].GetKind() == OR)
          {
@@ -19,7 +19,7 @@
          }
  
 --- ./src/simplifier/AlwaysTrue.h.orig	2011-05-01 06:48:53.000000000 -0600
-+++ ./src/simplifier/AlwaysTrue.h	2011-12-13 13:08:15.892474675 -0700
++++ ./src/simplifier/AlwaysTrue.h	2012-01-10 16:05:21.202610431 -0700
 @@ -88,7 +88,7 @@ public:
      else
        new_state = state;
@@ -30,7 +30,7 @@
          newChildren.push_back(visit(n[i],new_state,fromTo));
        }
 --- ./src/simplifier/MutableASTNode.h.orig	2011-03-29 07:18:23.000000000 -0600
-+++ ./src/simplifier/MutableASTNode.h	2011-12-13 13:08:15.893474673 -0700
++++ ./src/simplifier/MutableASTNode.h	2012-01-10 16:05:21.210610269 -0700
 @@ -46,12 +46,12 @@ public:
        vector<MutableASTNode *> tempChildren;
        tempChildren.reserve(n.Degree());
@@ -92,7 +92,7 @@
        all.clear();
      }
 --- ./src/simplifier/EstablishIntervals.h.orig	2011-08-08 23:15:54.000000000 -0600
-+++ ./src/simplifier/EstablishIntervals.h	2011-12-13 13:09:21.387399946 -0700
++++ ./src/simplifier/EstablishIntervals.h	2012-01-10 16:05:21.210610269 -0700
 @@ -117,7 +117,7 @@ namespace BEEV
        ASTVec new_children;
        new_children.reserve(result.GetChildren().size());
@@ -217,7 +217,7 @@
  
        likeAutoPtr.clear();
 --- ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp.orig	2010-11-27 20:45:32.000000000 -0700
-+++ ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp	2011-12-13 13:08:15.894474671 -0700
++++ ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp	2012-01-10 16:05:21.211610249 -0700
 @@ -204,8 +204,6 @@ Result bvArithmeticRightShiftBothWays(ve
  	assert(children[0]->getWidth() == children[1]->getWidth());
  	const unsigned MSBIndex = bitWidth-1;
@@ -268,16 +268,8 @@
  			}
  		}
  	}
-@@ -914,7 +906,6 @@ Result bvLeftShiftBothWays(vector<FixedB
- 			{
- 				op.setFixed(i - shiftIndex, true);
- 				op.setValue(i - shiftIndex, output.getValue(i));
--				result = CHANGED;
- 			}
- 		}
- 	}
---- ./src/simplifier/constantBitP/ConstantBitPropagation.cpp.orig	2011-09-11 06:53:41.000000000 -0600
-+++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp	2011-12-13 13:08:15.896474668 -0700
+--- ./src/simplifier/constantBitP/ConstantBitPropagation.cpp.orig	2012-01-01 19:28:47.000000000 -0700
++++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp	2012-01-10 16:05:21.212610229 -0700
 @@ -427,7 +427,7 @@ namespace simplifier
      void
      ConstantBitPropagation::scheduleDown(const ASTNode& n)
@@ -297,7 +289,7 @@
            if (!FixedBits::equals(*getUpdatedFixedBits(n[i]),
                childrenFixedBits[i]))
 --- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig	2010-11-27 20:45:32.000000000 -0700
-+++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp	2011-12-13 13:08:15.897474668 -0700
++++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp	2012-01-10 16:05:21.212610229 -0700
 @@ -110,8 +110,6 @@ void destroy(CBV a, CBV b, CBV c, CBV d)
  
  Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output)
@@ -439,8 +431,63 @@
  	assert(c0.getWidth() == c1.getWidth());
  
  	CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+--- ./src/simplifier/constantBitP/multiplication/ImplicationGraph.h.orig	2012-01-01 19:35:12.000000000 -0700
++++ ./src/simplifier/constantBitP/multiplication/ImplicationGraph.h	2012-01-10 16:12:04.745158953 -0700
+@@ -106,13 +106,13 @@ class ImplicationGraph
+ 			if (debug_multiply)
+ 			{
+ 				cout << "left";
+-				for (int i = 0; i < left.size(); i++)
++				for (size_t i = 0; i < left.size(); i++)
+ 				{
+ 
+ 					cout << "[" << i << ":" << left[i].size() << "] ";
+ 				}
+ 				cout << "right";
+-				for (int i = 0; i < right.size(); i++)
++				for (size_t i = 0; i < right.size(); i++)
+ 				{
+ 
+ 					cout << "[" << i << ":" << right[i].size() << "] ";
+@@ -512,8 +512,6 @@ public:
+ 		if (!ok)
+ 			return CONFLICT;
+ 
+-		Result r;
+-
+ 		bool changed = writeIn(left_assigned, left);
+ 		changed = writeIn(right_assigned, right) | changed;
+ 
+@@ -578,7 +576,7 @@ public:
+ 		}
+ 
+ 		bool allAlreadyMin = true;
+-		for (int i = 0; i < bitWidth; i++)
++		for (unsigned int i = 0; i < bitWidth; i++)
+ 			if (min[i] != 0)
+ 				allAlreadyMin = false;
+ 
+--- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig	2012-01-01 19:28:47.000000000 -0700
++++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp	2012-01-10 16:10:56.223982228 -0700
+@@ -172,14 +172,14 @@ Result bvUnsignedQuotientAndRemainder(ve
+ 	if (whatIs == QUOTIENT_IS_OUTPUT) {
+ 		setUnsignedMinMax(output, minQuotient, maxQuotient);
+ 
+-		for (int i = 0; i < width; i++)
++		for (unsigned int i = 0; i < width; i++)
+ 			CONSTANTBV::BitVector_Bit_On(maxRemainder, i);
+ 	}
+ 	else
+ 	{
+ 		setUnsignedMinMax(output, minRemainder, maxRemainder);
+ 
+-		for (int i =0; i < width;i++)
++		for (unsigned int i =0; i < width;i++)
+ 			CONSTANTBV::BitVector_Bit_On(maxQuotient,i);
+ 	}
+ 
 --- ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp.orig	2010-11-27 20:45:32.000000000 -0700
-+++ ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp	2011-12-13 13:08:15.897474668 -0700
++++ ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp	2012-01-10 16:05:21.213610209 -0700
 @@ -33,7 +33,6 @@ Result bvSubtractBothWays(vector<FixedBi
  	Addargs.push_back(&notB);
  	Addargs.push_back(&one);
@@ -475,9 +522,9 @@
  					changed = true;
  				}
  				else if (output.isFixed(column) && (output.getValue(column) != newResult))
---- ./src/simplifier/FindPureLiterals.h.orig	2011-02-25 20:56:39.000000000 -0700
-+++ ./src/simplifier/FindPureLiterals.h	2011-12-13 13:08:15.897474668 -0700
-@@ -108,7 +108,7 @@ public:
+--- ./src/simplifier/FindPureLiterals.h.orig	2011-12-19 17:30:14.000000000 -0700
++++ ./src/simplifier/FindPureLiterals.h	2012-01-10 16:05:21.214610188 -0700
+@@ -109,7 +109,7 @@ public:
      {
      case AND:
      case OR:
@@ -486,7 +533,7 @@
          build(n[i],polarity);
        break;
  
-@@ -119,7 +119,7 @@ public:
+@@ -120,7 +120,7 @@ public:
  
      default:
          polarity = bothPolarity; // both
@@ -496,7 +543,7 @@
        break;
      }
 --- ./src/simplifier/VariablesInExpression.cpp.orig	2011-02-01 05:41:57.000000000 -0700
-+++ ./src/simplifier/VariablesInExpression.cpp	2011-12-13 13:08:15.898474667 -0700
++++ ./src/simplifier/VariablesInExpression.cpp	2012-01-10 16:05:21.214610188 -0700
 @@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbo
  	}
  
@@ -524,9 +571,9 @@
  			if (i!=0 && av[i] == av[i-1])
  				continue;
  
---- ./src/simplifier/SubstitutionMap.cpp.orig	2011-05-01 08:20:34.000000000 -0600
-+++ ./src/simplifier/SubstitutionMap.cpp	2011-12-13 13:08:15.899474666 -0700
-@@ -366,7 +366,7 @@ void SubstitutionMap::buildDepends(const
+--- ./src/simplifier/SubstitutionMap.cpp.orig	2011-12-28 20:17:45.000000000 -0700
++++ ./src/simplifier/SubstitutionMap.cpp	2012-01-10 16:05:21.215610168 -0700
+@@ -199,7 +199,7 @@ void SubstitutionMap::buildDepends(const
  	vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av);
  
  	sort(av.begin(), av.end());
@@ -535,9 +582,9 @@
  	{
  		if (i!=0 && av[i] == av[i-1])
  			continue; // Treat it like a set of Symbol* in effect.
---- ./src/simplifier/simplifier.cpp.orig	2011-11-18 04:12:27.000000000 -0700
-+++ ./src/simplifier/simplifier.cpp	2011-12-13 13:08:15.900474665 -0700
-@@ -250,7 +250,7 @@ namespace BEEV
+--- ./src/simplifier/simplifier.cpp.orig	2012-01-05 06:04:33.000000000 -0700
++++ ./src/simplifier/simplifier.cpp	2012-01-10 16:10:08.282375196 -0700
+@@ -241,7 +241,7 @@ namespace BEEV
          assert(false);
        }
  
@@ -546,7 +593,7 @@
        {
          checkIfInSimplifyMap(n[i], visited);
        }
-@@ -525,6 +525,7 @@ namespace BEEV
+@@ -516,6 +516,7 @@ namespace BEEV
        return getConstantBit(n[0], i);
  
      assert(false);
@@ -554,7 +601,7 @@
    }
  
    ASTNode
-@@ -1293,7 +1294,7 @@ namespace BEEV
+@@ -1284,7 +1285,7 @@ namespace BEEV
      else
        {
          ASTVec newC;
@@ -563,7 +610,7 @@
            {
              newC.push_back(SimplifyFormula(a[i], false, VarConstMap));
            }
-@@ -1655,9 +1656,9 @@ namespace BEEV
+@@ -1646,9 +1647,9 @@ namespace BEEV
      assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
      const int inputValueWidth = output.GetValueWidth();
  
@@ -576,7 +623,7 @@
      if (BVMULT == output.GetKind())
        maxLength = lengthA + lengthB;
      else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
-@@ -1685,7 +1686,7 @@ namespace BEEV
+@@ -1676,7 +1677,7 @@ namespace BEEV
    {
      const ASTNode a = children[0];
      const ASTNode b = children[1];
@@ -585,7 +632,7 @@
      ASTNode output;
  
      assert(b.isConstant());
-@@ -1716,7 +1717,7 @@ namespace BEEV
+@@ -1707,7 +1708,7 @@ namespace BEEV
    {
      const ASTNode a = children[0];
      const ASTNode b = children[1];
@@ -594,7 +641,7 @@
      ASTNode output;
  
      assert(b.isConstant());
-@@ -1897,7 +1898,7 @@ namespace BEEV
+@@ -1888,7 +1889,7 @@ namespace BEEV
      //I haven't measured if this is worth the expense.
        {
          bool notSimplified = false;
@@ -603,7 +650,7 @@
            if (inputterm[i].GetType() != ARRAY_TYPE)
              if (!hasBeenSimplified(inputterm[i]))
                {
-@@ -2238,7 +2239,6 @@ namespace BEEV
+@@ -2229,7 +2230,6 @@ namespace BEEV
          case BVEXTRACT:
            {
              const unsigned innerLow = a0[2].GetUnsignedConst();
@@ -611,7 +658,7 @@
  
              output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow),
                  _bm->CreateBVConst(32, j_val + innerLow));
-@@ -2638,7 +2638,7 @@ namespace BEEV
+@@ -2629,7 +2629,7 @@ namespace BEEV
              assert(BVTypeCheck(output));
  
              // If the leading bits are zero. Replace it by a concat with zero.
@@ -620,7 +667,7 @@
              if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0))
                {
                  // i contains the number of leading zeroes.
-@@ -2660,13 +2660,13 @@ namespace BEEV
+@@ -2651,13 +2651,13 @@ namespace BEEV
            }
          if (output.GetKind() == BVAND)
            {
@@ -637,7 +684,7 @@
                  for (j = 0; j < n.GetValueWidth(); j++)
                    if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j))
                      break;
-@@ -2683,7 +2683,7 @@ namespace BEEV
+@@ -2674,7 +2674,7 @@ namespace BEEV
                      //cerr << "old" << output;
                      ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes);
                      ASTVec newChildren;
@@ -646,8 +693,8 @@
                        newChildren.push_back(
                            nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i],
                                _bm->CreateBVConst(32, output.GetValueWidth() - 1),
---- ./src/simplifier/consteval.cpp.orig	2011-06-15 21:54:40.000000000 -0600
-+++ ./src/simplifier/consteval.cpp	2011-12-13 13:08:15.900474665 -0700
+--- ./src/simplifier/consteval.cpp.orig	2011-12-28 19:00:01.000000000 -0700
++++ ./src/simplifier/consteval.cpp	2012-01-10 16:05:21.217610127 -0700
 @@ -43,7 +43,7 @@ namespace BEEV
  
      ASTVec children;
@@ -657,8 +704,8 @@
      {
      	if (input_children[i].isConstant())
      		children.push_back(input_children[i]);
---- ./src/simplifier/SubstitutionMap.h.orig	2011-04-12 20:00:29.000000000 -0600
-+++ ./src/simplifier/SubstitutionMap.h	2011-12-13 13:08:15.901474664 -0700
+--- ./src/simplifier/SubstitutionMap.h.orig	2011-12-28 20:17:45.000000000 -0700
++++ ./src/simplifier/SubstitutionMap.h	2012-01-10 16:05:21.218610106 -0700
 @@ -40,7 +40,7 @@ class SubstitutionMap {
  	void loops_helper(const set<ASTNode>& varsToCheck, set<ASTNode>& visited);
  	bool loops(const ASTNode& n0, const ASTNode& n1);
@@ -668,8 +715,8 @@
  public:
  
  	bool hasUnappliedSubstitutions()
---- ./src/simplifier/RemoveUnconstrained.cpp.orig	2011-08-05 22:02:44.000000000 -0600
-+++ ./src/simplifier/RemoveUnconstrained.cpp	2011-12-13 13:08:15.901474664 -0700
+--- ./src/simplifier/RemoveUnconstrained.cpp.orig	2011-12-28 19:00:01.000000000 -0700
++++ ./src/simplifier/RemoveUnconstrained.cpp	2012-01-10 16:05:21.218610106 -0700
 @@ -60,7 +60,7 @@ namespace BEEV
  
    bool allChildrenAreUnconstrained(vector <MutableASTNode*> children)
@@ -760,7 +807,7 @@
                  assert(children[0] == var); // It can't be anywhere else.
  
 --- ./src/absrefine_counterexample/CounterExample.cpp.orig	2011-11-10 06:01:41.000000000 -0700
-+++ ./src/absrefine_counterexample/CounterExample.cpp	2011-12-13 13:08:15.902474663 -0700
++++ ./src/absrefine_counterexample/CounterExample.cpp	2012-01-10 16:05:21.219610086 -0700
 @@ -46,7 +46,7 @@ namespace BEEV
          assert(symbol.GetKind() == SYMBOL);
          vector<bool>  bitVector_array(symbolWidth,false);
@@ -779,8 +826,8 @@
          {
          if (v[i] == ~((unsigned)0)) // nb. special value.
            continue;
---- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig	2011-08-30 22:02:27.000000000 -0600
-+++ ./src/absrefine_counterexample/AbstractionRefinement.cpp	2011-12-13 13:08:15.902474663 -0700
+--- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig	2012-01-05 06:04:33.000000000 -0700
++++ ./src/absrefine_counterexample/AbstractionRefinement.cpp	2012-01-10 16:05:21.220610066 -0700
 @@ -35,7 +35,7 @@ namespace BEEV
              {
                  assert(a.GetKind() == SYMBOL);
@@ -859,8 +906,8 @@
                              {
                                  const ASTNode& index_j = listOfIndices[j];
  
---- ./src/to-sat/ASTNode/ToSAT.cpp.orig	2011-02-01 22:39:54.000000000 -0700
-+++ ./src/to-sat/ASTNode/ToSAT.cpp	2011-12-13 13:08:15.903474662 -0700
+--- ./src/to-sat/ASTNode/ToSAT.cpp.orig	2011-12-28 19:00:01.000000000 -0700
++++ ./src/to-sat/ASTNode/ToSAT.cpp	2012-01-10 16:05:21.220610066 -0700
 @@ -52,7 +52,7 @@ namespace BEEV
  
          // Copies the symbol into the map that is used to build the counter example.
@@ -897,8 +944,8 @@
        {
          ClauseList *cl = (*it).second;
  	    sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm);
---- ./src/to-sat/ASTNode/ToCNF.cpp.orig	2011-01-23 06:08:12.000000000 -0700
-+++ ./src/to-sat/ASTNode/ToCNF.cpp	2011-12-13 13:08:15.903474663 -0700
+--- ./src/to-sat/ASTNode/ToCNF.cpp.orig	2011-12-28 19:00:01.000000000 -0700
++++ ./src/to-sat/ASTNode/ToCNF.cpp	2012-01-10 16:05:21.221610046 -0700
 @@ -250,12 +250,14 @@ namespace BEEV
      return psi;
    } //End of SINGLETON()
@@ -914,143 +961,526 @@
  
    //########################################
    //########################################
---- ./src/to-sat/BitBlaster.cpp.orig	2011-11-15 03:40:28.000000000 -0700
-+++ ./src/to-sat/BitBlaster.cpp	2011-12-13 13:08:15.904474662 -0700
-@@ -299,7 +299,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
- template <class BBNode, class BBNodeManagerT>
- bool BitBlaster<BBNode,BBNodeManagerT>::isConstant(const BBNodeVec& v)
- {
--  for (int i =0; i < v.size();i++)
-+  for (size_t i =0; i < v.size();i++)
+--- ./src/to-sat/BitBlaster.cpp.orig	2012-01-09 20:03:23.000000000 -0700
++++ ./src/to-sat/BitBlaster.cpp	2012-01-10 16:06:28.158957729 -0700
+@@ -311,7 +311,7 @@ namespace BEEV
+     bool
+     BitBlaster<BBNode, BBNodeManagerT>::isConstant(const BBNodeVec& v)
      {
+-      for (int i = 0; i < v.size(); i++)
++      for (size_t i = 0; i < v.size(); i++)
+         {
          if (v[i] != nf->getTrue() && v[i] != nf->getFalse())
            return false;
-@@ -322,7 +322,7 @@ ASTNode BitBlaster<BBNode,BBNodeManagerT
+@@ -334,7 +334,7 @@ namespace BEEV
  
-   CBV bv = CONSTANTBV::BitVector_Create(v.size(),true);
+       CBV bv = CONSTANTBV::BitVector_Create(v.size(), true);
  
--  for (int i =0; i < v.size();i++)
-+  for (size_t i =0; i < v.size();i++)
-       if (v[i] == nf->getTrue())
-         CONSTANTBV::BitVector_Bit_On(bv,i);
+-      for (int i = 0; i < v.size(); i++)
++      for (size_t i = 0; i < v.size(); i++)
+         if (v[i] == nf->getTrue())
+           CONSTANTBV::BitVector_Bit_On(bv, i);
  
-@@ -640,14 +640,14 @@ const BBNodeVec BitBlaster<BBNode,BBNode
- 	            {
- 	              // Add all the children up using an addition network.
- 	              vector<BBNodeVec> results;
--	              for (int i=0; i < term.Degree();i++)
-+	              for (size_t i=0; i < term.Degree();i++)
- 	                results.push_back(BBTerm(term[i], support));
+@@ -670,14 +670,14 @@ namespace BEEV
+           {
+           // Add all the children up using an addition network.
+           vector<BBNodeVec> results;
+-          for (int i = 0; i < term.Degree(); i++)
++          for (size_t i = 0; i < term.Degree(); i++)
+             results.push_back(BBTerm(term[i], support));
  
- 	              const int bitWidth = term[0].GetValueWidth();
- 	              std::vector<stack<BBNode> > products(bitWidth);
- 	              for (int i=0; i < bitWidth;i++)
- 	                {
--	                  for (int j=0; j < results.size();j++)
-+	                  for (size_t j=0; j < results.size();j++)
- 	                    products[i].push(results[j][i]);
- 	                }
+-          const int bitWidth = term[0].GetValueWidth();
++          const unsigned int bitWidth = term[0].GetValueWidth();
+           std::vector<list<BBNode> > products(bitWidth);
+-          for (int i = 0; i < bitWidth; i++)
++          for (unsigned int i = 0; i < bitWidth; i++)
+             {
+-            for (int j = 0; j < results.size(); j++)
++            for (size_t j = 0; j < results.size(); j++)
+               products[i].push_back(results[j][i]);
+             }
  
-@@ -1070,7 +1070,7 @@ void convert(const BBNodeVec& v, BBNodeM
- 	const BBNode& BBTrue = nf->getTrue();
- 	const BBNode& BBFalse = nf->getFalse();
+@@ -1157,7 +1157,7 @@ namespace BEEV
+       const BBNode& BBTrue = nf->getTrue();
+       const BBNode& BBFalse = nf->getFalse();
  
--	for (int i =0; i < v.size(); i++)
-+	for (size_t i =0; i < v.size(); i++)
- 	{
- 		if (v[i] == BBTrue)
- 			result[i] = ONE_MT;
-@@ -1082,7 +1082,7 @@ void convert(const BBNodeVec& v, BBNodeM
+-      for (int i = 0; i < v.size(); i++)
++      for (size_t i = 0; i < v.size(); i++)
+         {
+         if (v[i] == BBTrue)
+           result[i] = ONE_MT;
+@@ -1169,7 +1169,7 @@ namespace BEEV
  
- 	// find runs of ones.
- 	int lastOne=-1;
--	for (int i =0; i < v.size(); i++)
-+	for (size_t i =0; i < v.size(); i++)
- 	{
- 		assert(result[i] != MINUS_ONE_MT);
+       // find runs of ones.
+       int lastOne = -1;
+-      for (int i = 0; i < v.size(); i++)
++      for (size_t i = 0; i < v.size(); i++)
+         {
+         assert(result[i] != MINUS_ONE_MT);
  
-@@ -1092,7 +1092,7 @@ void convert(const BBNodeVec& v, BBNodeM
- 		if (result[i] != ONE_MT && lastOne != -1 && (i-lastOne >=3))
- 		{
- 			result[lastOne] = MINUS_ONE_MT;
--			for (int j = lastOne+1; j<i;j++)
-+			for (size_t j = lastOne+1; j<i;j++)
- 				result[j] = ZERO_MT;
- 			// Should this be lastOne = i?
- 			lastOne = i;
-@@ -1105,7 +1105,7 @@ void convert(const BBNodeVec& v, BBNodeM
- 	if (lastOne != -1 && (v.size() -lastOne >1))
- 	{
- 		result[lastOne] = MINUS_ONE_MT;
--		for (int j = lastOne+1; j< v.size();j++)
-+		for (size_t j = lastOne+1; j< v.size();j++)
- 			result[j] = ZERO_MT;
- 	}
- }
-@@ -1310,7 +1310,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
-                         cerr << "["<< ms.columnL[i] << ":"<< ms.columnH[i] << "]["<< ms.sumL[i] << ":" << ms.sumH[i] << "]";
-                 }
+@@ -1179,7 +1179,7 @@ namespace BEEV
+         if (result[i] != ONE_MT && lastOne != -1 && (i - lastOne >= 3))
+           {
+           result[lastOne] = MINUS_ONE_MT;
+-          for (int j = lastOne + 1; j < i; j++)
++          for (size_t j = lastOne + 1; j < i; j++)
+             result[j] = ZERO_MT;
+           // Should this be lastOne = i?
+           lastOne = i;
+@@ -1193,7 +1193,7 @@ namespace BEEV
+       if (lastOne != -1 && (v.size() - lastOne > 1))
+         {
+         result[lastOne] = MINUS_ONE_MT;
+-        for (int j = lastOne + 1; j < v.size(); j++)
++        for (size_t j = lastOne + 1; j < v.size(); j++)
+           result[j] = ZERO_MT;
+         }
+     }
+@@ -1235,7 +1235,7 @@ namespace BEEV
+     BitBlaster<BBNode, BBNodeManagerT>::buildAdditionNetworkResult(list<BBNode>* products, set<BBNode>& support,
+         const ASTNode& n)
+     {
+-      const int bitWidth = n.GetValueWidth();
++      const unsigned int bitWidth = n.GetValueWidth();
  
--                if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
-+                if (((int)products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
-                 {
-                         if (debug_bounds)
-                                 cerr << "S";
-@@ -1361,7 +1361,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
- 	 }
+       // If we have details of the partial products which can be true,
+       int ignore = -1;
+@@ -1244,7 +1244,7 @@ namespace BEEV
+         ms = NULL;
  
- 	 BBNodeVec notY;
--	 for (int i =0 ; i < y.size();i++)
-+	 for (size_t i =0 ; i < y.size();i++)
- 	 {
- 		 notY.push_back(nf->CreateNode(NOT,y[i]));
- 	 }
-@@ -1414,7 +1414,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
- 		   t_products[i].push_back(BBFalse);
+       BBNodeVec results;
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+         {
  
- 		 sort(t_products[i].begin(), t_products[i].end());
--		 for (int j=0; j < t_products[i].size();j++)
-+		 for (size_t j=0; j < t_products[i].size();j++)
- 		     products[i].push(t_products[i][j]);
- 	 }
-   }
-@@ -1488,7 +1488,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+         buildAdditionNetworkResult(products[i], products[i+1], support, (i + 1 == bitWidth), (ms != NULL && (ms->sumH[i] == 0)));
+@@ -1254,7 +1254,7 @@ namespace BEEV
+         }
+ 
+       assert(products[bitWidth].size() ==0); // products[bitwidth] is defined but should never be used.
+-      assert(results.size() == ((unsigned)bitWidth));
++      assert(results.size() == bitWidth);
+       return results;
+     }
+ 
+@@ -1356,7 +1356,7 @@ namespace BEEV
+     BitBlaster<BBNode, BBNodeManagerT>::multWithBounds(const ASTNode&n, list<BBNode>* products,
+         BBNodeSet& toConjoinToTop)
+     {
+-      const int bitWidth = n.GetValueWidth();
++      const unsigned int bitWidth = n.GetValueWidth();
+ 
+       int ignored=0;
+       assert(multiplication_upper_bound);
+@@ -1365,7 +1365,7 @@ namespace BEEV
+ 
+ 
+       // If all of the partial products in the column must be zero, then replace
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+         {
+         if (conjoin_to_top && ms.columnH[i] == 0)
+           {
+@@ -1387,7 +1387,7 @@ namespace BEEV
+         }
+ 
+       vector<BBNode> prior;
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+         {
+         if (debug_bounds)
+           {
+@@ -1407,7 +1407,7 @@ namespace BEEV
+       if (debug_bitblaster)
+         cerr << endl << endl;
+ 
+-      assert(result.size() == ((unsigned)bitWidth));
++      assert(result.size() == bitWidth);
+       return result;
+     }
+ 
+@@ -1431,7 +1431,7 @@ namespace BEEV
+         }
+ 
+       BBNodeVec notY;
+-      for (int i = 0; i < y.size(); i++)
++      for (size_t i = 0; i < y.size(); i++)
+         {
+         notY.push_back(nf->CreateNode(NOT, y[i]));
+         }
+@@ -1484,7 +1484,7 @@ namespace BEEV
+           t_products[i].push_back(BBFalse);
+ 
+         sort(t_products[i].begin(), t_products[i].end());
+-        for (int j = 0; j < t_products[i].size(); j++)
++        for (size_t j = 0; j < t_products[i].size(); j++)
+           products[i].push_back(t_products[i][j]);
+         }
+     }
+@@ -1542,13 +1542,13 @@ namespace BEEV
+           assert(ms->x.getWidth() == ms->y.getWidth());
+           assert(ms->r.getWidth() == ms->y.getWidth());
+           assert(ms->r.getWidth() == (int)ms->bitWidth);
+-          }
+ 
+-        for (int i = 0; i < n.GetValueWidth(); i++)
+-          if (ms->sumH[i] == 0)
+-            highestZero = i;
++          for (unsigned int i = 0; i < n.GetValueWidth(); i++)
++            if (ms->sumH[i] == 0)
++              highestZero = (int)i;
+ 
+-        return ms;
++          return ms;
++          }
+         }
+ 
+       return NULL;
+@@ -1560,7 +1560,7 @@ namespace BEEV
+     BitBlaster<BBNode, BBNodeManagerT>::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support,
+         const ASTNode&n)
+     {
+-      const int bitWidth = n.GetValueWidth();
++      const unsigned int bitWidth = n.GetValueWidth();
+ 
+       // If we have details of the partial products which can be true,
+       int highestZero = -1;
+@@ -1572,7 +1572,7 @@ namespace BEEV
+ 
+       BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin()));       // start prod with first partial product.
+ 
+-      for (int i = 1; i < bitWidth; i++)       // start loop at next bit.
++      for (unsigned int i = 1; i < bitWidth; i++)       // start loop at next bit.
+         {
+         const BBNode& xit = x[i];
+ 
+@@ -1589,7 +1589,7 @@ namespace BEEV
+         BBNodeVec pprod = BBAndBit(ycopy, xit);
+ 
+         // Iterate through from the current location upwards, setting anything to zero that can be..
+-        if (ms != NULL && highestZero >= i)
++        if (ms != NULL && highestZero >= (int)i)
+           {
+           for (int column = i; column <= highestZero; column++)
+             {
+@@ -1614,7 +1614,7 @@ namespace BEEV
      {
  
        // Add the carry from the prior column. i.e. each second sorted formula.
 -      for (int k = 1; k < priorSorted.size(); k += 2)
 +      for (size_t k = 1; k < priorSorted.size(); k += 2)
          {
-           current.push(priorSorted[k]);
+         current.push_back(priorSorted[k]);
          }
-@@ -1570,7 +1570,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+@@ -1694,7 +1694,7 @@ namespace BEEV
          FixedBits* b = cb->fixedMap->map->find(n)->second;
          for (int i = 0; i < b->getWidth(); i++)
            {
--            if (b->isFixed(i))
-+            if (b->isFixed(i)) {
-               if (b->getValue(i))
-                 {
-                   assert(v[i]== BBTrue);
-@@ -1587,6 +1587,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+-          if (b->isFixed(i))
++          if (b->isFixed(i)) {
+             if (b->getValue(i))
+               {
+               assert(v[i]== BBTrue);
+@@ -1711,6 +1711,7 @@ namespace BEEV
  
-                   assert(v[i]== BBFalse);
-                 }
-+              }
+               assert(v[i]== BBFalse);
+               }
++            }
            }
-       }
-   }
-@@ -1701,7 +1702,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
+         }
+     }
+@@ -1734,7 +1735,7 @@ namespace BEEV
+         y = _x;
+         }
  
- 	// check if y is already zero.
- 	bool isZero=true;
--	for (int i =0; i < rwidth;i++)
-+	for (unsigned int i =0; i < rwidth;i++)
-           if (y[i] != nf->getFalse())
+-      const int bitWidth = n.GetValueWidth();
++      const unsigned int bitWidth = n.GetValueWidth();
+       assert(x.size() == bitWidth);
+       assert(y.size() == bitWidth);
+ 
+@@ -1762,7 +1763,7 @@ namespace BEEV
+         mult_Booth(_x, _y, support, n[0], n[1], products.data(), n);
+         vector<BBNode> prior;
+ 
+-        for (int i = 0; i < bitWidth; i++)
++        for (unsigned int i = 0; i < bitWidth; i++)
            {
-             isZero = false;
+           vector<BBNode> output;
+           mult_BubbleSorterWithBounds(support, products[i], output, prior);
+@@ -1824,18 +1825,18 @@ namespace BEEV
+     vector<BBNode> b;
+ 
+     // half way rounded up.
+-    const int halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) );
+-    for (int i =0; i < halfWay;i++)
++    const size_t halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) );
++    for (size_t i =0; i < halfWay;i++)
+         a.push_back(in[i]);
+ 
+-    for (int i =halfWay; i < in.size();i++)
++    for (size_t i =halfWay; i < in.size();i++)
+         b.push_back(in[i]);
+ 
+     assert(a.size() >= b.size());
+     assert(a.size() + b.size() == in.size());
+     vector <BBNode> result=  mergeSorted(batcher(a), batcher(b));
+ 
+-    for (int k = 0; k < result.size(); k++)
++    for (size_t k = 0; k < result.size(); k++)
+       assert(!result[k].IsNull());
+ 
+     assert(result.size() == in.size());
+@@ -1867,7 +1868,7 @@ namespace BEEV
+       assert(sorted.size() == toSort.size());
+ 
+       vector<BBNode> sortedCarryIn;
+-      for (int k = 1; k < priorSorted.size(); k += 2)
++      for (size_t k = 1; k < priorSorted.size(); k += 2)
+         {
+         sortedCarryIn.push_back(priorSorted[k]);
+         }
+@@ -1905,11 +1906,11 @@ namespace BEEV
+   BBNodeVec
+   BitBlaster<BBNode, BBNodeManagerT>::v6(list<BBNode>* products, set<BBNode>& support,  const ASTNode&n)
+   {
+-    const int bitWidth = n.GetValueWidth();
++    const unsigned int bitWidth = n.GetValueWidth();
+ 
+   vector<BBNode> prior;
+ 
+-  for (int i = 0; i < bitWidth; i++)
++  for (unsigned int i = 0; i < bitWidth; i++)
+     {
+         vector<BBNode> output;
+         sortingNetworkAdd(support,  products[i], output ,prior);
+@@ -1928,22 +1929,21 @@ namespace BEEV
+     BBNodeVec
+     BitBlaster<BBNode, BBNodeManagerT>::v9(list<BBNode>* products, set<BBNode>& support,const ASTNode&n)
+     {
+-    const int bitWidth = n.GetValueWidth();
++    const unsigned int bitWidth = n.GetValueWidth();
+ 
+     vector< vector< BBNode> > toAdd(bitWidth);
+ 
+-    for (int column = 0; column < bitWidth; column++)
++    for (unsigned int column = 0; column < bitWidth; column++)
+       {
+           vector<BBNode> sorted; // The current column (sorted) gets put into here.
+           vector<BBNode> prior; // Prior is always empty in this..
+ 
+-          const int size=  products[column].size();
+           sortingNetworkAdd(support,  products[column], sorted ,prior);
+ 
+           assert(products[column].size() == 1);
+           assert(sorted.size() == size);
+ 
+-          for (int k = 2; k <= sorted.size(); k++)
++          for (size_t k = 2; k <= sorted.size(); k++)
+             {
+               BBNode part;
+               if (k==sorted.size())
+@@ -1958,7 +1958,7 @@ namespace BEEV
+                   continue; // shortcut.
+                 }
+ 
+-              int position =k;
++              size_t position =k;
+               int increment =1;
+               while (position != 0)
+                 {
+@@ -1973,12 +1973,12 @@ namespace BEEV
+                 }
+             }
+ 
+-          for (int carry_column =column+1; carry_column < bitWidth; carry_column++)
++          for (unsigned int carry_column =column+1; carry_column < bitWidth; carry_column++)
+             {
+               if (toAdd[carry_column].size() ==0)
+                 continue ;
+               BBNode disjunct = BBFalse;
+-              for (int l = 0; l < toAdd[carry_column].size();l++)
++              for (size_t l = 0; l < toAdd[carry_column].size();l++)
+                     {
+                         disjunct = nf->CreateNode(OR,disjunct,toAdd[carry_column][l]);
+                     }
+@@ -1988,7 +1988,7 @@ namespace BEEV
+               toAdd[carry_column].clear();
+             }
+       }
+-    for (int i = 0; i < bitWidth; i++)
++    for (unsigned int i = 0; i < bitWidth; i++)
+       {
+         assert(toAdd[i].size() == 0);
+       }
+@@ -2002,7 +2002,7 @@ namespace BEEV
+   BBNodeVec
+   BitBlaster<BBNode, BBNodeManagerT>::v7(list<BBNode>* products, set<BBNode>& support, const ASTNode&n)
+   {
+-    const int bitWidth = n.GetValueWidth();
++    const unsigned int bitWidth = n.GetValueWidth();
+ 
+     // If we have details of the partial products which can be true,
+     int ignore = -1;
+@@ -2014,13 +2014,13 @@ namespace BEEV
+       std::vector<list<BBNode> > later(bitWidth+1);
+       std::vector<list<BBNode> > next(bitWidth+1);
+ 
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+           {
+               next[i+1].clear();
+               buildAdditionNetworkResult(products[i], next[i + 1], support, bitWidth == i+1, (ms!=NULL && (ms->sumH[i]==0)));
+ 
+               // Calculate the carries of carries.
+-              for (int j = i + 1; j < bitWidth; j++)
++              for (unsigned int j = i + 1; j < bitWidth; j++)
+                   {
+                       if (next[j].size() == 0)
+                           break;
+@@ -2030,7 +2030,7 @@ namespace BEEV
+                   }
+ 
+               // Put the carries of the carries away until later.
+-              for (int j = i + 1; j < bitWidth; j++)
++              for (unsigned int j = i + 1; j < bitWidth; j++)
+                   {
+                       if (next[j].size() == 0)
+                           break;
+@@ -2041,7 +2041,7 @@ namespace BEEV
+           }
+ 
+ 
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+       {
+               // Copy all the laters into products
+               while(later[i].size() > 0)
+@@ -2052,7 +2052,7 @@ namespace BEEV
+       }
+ 
+       BBNodeVec results;
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+       {
+ 
+               buildAdditionNetworkResult((products[i]), (products[i + 1]), support, bitWidth == i+1, false);
+@@ -2062,7 +2062,7 @@ namespace BEEV
+           products[i].pop_back();
+       }
+ 
+-      assert(results.size() == ((unsigned)bitWidth));
++      assert(results.size() == bitWidth);
+       return results;
+   }
+ 
+@@ -2071,7 +2071,7 @@ namespace BEEV
+   BBNodeVec
+   BitBlaster<BBNode, BBNodeManagerT>::v8(list<BBNode>* products, set<BBNode>& support, const ASTNode&n)
+   {
+-    const int bitWidth = n.GetValueWidth();
++    const unsigned int bitWidth = n.GetValueWidth();
+ 
+     // If we have details of the partial products which can be true,
+     int ignore = -1;
+@@ -2084,14 +2084,14 @@ namespace BEEV
+       std::vector<list<BBNode> > later(bitWidth+1); // +1 then ignore the topmost.
+       std::vector<list<BBNode> > next(bitWidth+1);
+ 
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+           {
+               // Put all the products into next.
+               next[i+1].clear();
+               buildAdditionNetworkResult((products[i]), (next[i + 1]), support, i+1 ==bitWidth, (ms!=NULL && (ms->sumH[i]==0)));
+ 
+               // Calculate the carries of carries.
+-              for (int j = i + 1; j < bitWidth; j++)
++              for (unsigned int j = i + 1; j < bitWidth; j++)
+                   {
+                       if (next[j].size() == 0)
+                           break;
+@@ -2101,7 +2101,7 @@ namespace BEEV
+                   }
+ 
+               // Put the carries of the carries away until later.
+-              for (int j = i + 1; j < bitWidth; j++)
++              for (unsigned int j = i + 1; j < bitWidth; j++)
+                   {
+                       if (next[j].size() == 0)
+                           break;
+@@ -2112,7 +2112,7 @@ namespace BEEV
+           }
+ 
+ 
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+       {
+               // Copy all the laters into products
+               while(later[i].size() > 0)
+@@ -2123,14 +2123,14 @@ namespace BEEV
+       }
+ 
+       BBNodeVec results;
+-      for (int i = 0; i < bitWidth; i++)
++      for (unsigned int i = 0; i < bitWidth; i++)
+       {
+           buildAdditionNetworkResult(products[i], products[i + 1], support, i+1 ==bitWidth, false);
+           results.push_back(products[i].back());
+           products[i].pop_back();
+       }
+ 
+-      assert(results.size() == ((unsigned)bitWidth));
++      assert(results.size() == bitWidth);
+       return results;
+   }
+ 
+@@ -2142,7 +2142,7 @@ namespace BEEV
+     {
+       vector<BBNode> result(in);
+ 
+-      for (int i = 2; i < in.size(); i =i+ 2)
++      for (size_t i = 2; i < in.size(); i =i+ 2)
+         {
+             BBNode a = in[i-1];
+             BBNode b = in[i];
+@@ -2179,7 +2179,7 @@ namespace BEEV
+         {
+           vector <BBNode> evenL;
+           vector <BBNode> oddL;
+-          for (int i =0; i < in1.size();i++)
++          for (size_t i =0; i < in1.size();i++)
+             {
+                 if (i%2 ==0)
+                   evenL.push_back(in1[i]);
+@@ -2189,7 +2189,7 @@ namespace BEEV
+ 
+           vector <BBNode> evenR;  // Take the even of each.
+           vector <BBNode> oddR;   // Take the odd of each
+-            for (int i =0; i < in2.size();i++)
++            for (size_t i =0; i < in2.size();i++)
+               {
+                   if (i%2 ==0)
+                     evenR.push_back(in2[i]);
+@@ -2200,7 +2200,7 @@ namespace BEEV
+             vector <BBNode> even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR);
+             vector <BBNode> odd = oddL.size() < oddR.size() ? mergeSorted(oddR,oddL) : mergeSorted(oddL,oddR);
+ 
+-            for (int i =0; i < std::max(even.size(),odd.size());i++)
++            for (size_t i =0; i < std::max(even.size(),odd.size());i++)
+               {
+                 if (even.size() > i)
+                   result.push_back(even[i]);
+@@ -2245,7 +2245,7 @@ namespace BEEV
+ 
+       // check if y is already zero.
+       bool isZero = true;
+-      for (int i = 0; i < rwidth; i++)
++      for (unsigned int i = 0; i < rwidth; i++)
+         if (y[i] != nf->getFalse())
+           {
+           isZero = false;
 --- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig	2011-02-01 22:39:54.000000000 -0700
-+++ ./src/to-sat/AIG/BBNodeManagerAIG.h	2011-12-13 13:08:15.905474660 -0700
++++ ./src/to-sat/AIG/BBNodeManagerAIG.h	2012-01-10 16:05:21.224609986 -0700
 @@ -142,7 +142,7 @@ public:
                  Aig_Obj_t * pNode;
                  assert (children.size() != 0);
@@ -1060,8 +1490,8 @@
                    assert(!children[i].IsNull());
  
                  switch (kind)
---- ./src/to-sat/AIG/ToSATAIG.cpp.orig	2011-11-27 19:55:18.000000000 -0700
-+++ ./src/to-sat/AIG/ToSATAIG.cpp	2011-12-13 13:08:15.905474660 -0700
+--- ./src/to-sat/AIG/ToSATAIG.cpp.orig	2011-12-31 07:51:52.000000000 -0700
++++ ./src/to-sat/AIG/ToSATAIG.cpp	2012-01-10 16:05:21.225609966 -0700
 @@ -126,7 +126,7 @@ namespace BEEV
                          if (it != nodeToSATVar.end())
                              {
@@ -1134,9 +1564,9 @@
                                              {
                                                  SATSolver::Var var = v_a[i];
                                                  value.push(SATSolver::mkLit(var, false));
---- ./src/c_interface/c_interface.cpp.orig	2011-11-10 06:01:41.000000000 -0700
-+++ ./src/c_interface/c_interface.cpp	2011-12-13 13:08:15.906474658 -0700
-@@ -613,7 +613,6 @@ void vc_printCounterExample(VC vc) {
+--- ./src/c_interface/c_interface.cpp.orig	2011-12-21 22:12:52.000000000 -0700
++++ ./src/c_interface/c_interface.cpp	2012-01-10 16:05:21.225609966 -0700
+@@ -516,7 +516,6 @@ void vc_printCounterExample(VC vc) {
  
  Expr vc_getCounterExample(VC vc, Expr e) {
    nodestar a = (nodestar)e;
@@ -1144,7 +1574,7 @@
    ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
  
    bool t = false;
-@@ -626,7 +625,6 @@ Expr vc_getCounterExample(VC vc, Expr e)
+@@ -529,7 +528,6 @@ Expr vc_getCounterExample(VC vc, Expr e)
  
  void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size) {
    nodestar a = (nodestar)e;
@@ -1152,7 +1582,7 @@
    ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
  
    bool t = false;
-@@ -646,7 +644,6 @@ void vc_getCounterExampleArray(VC vc, Ex
+@@ -549,7 +547,6 @@ void vc_getCounterExampleArray(VC vc, Ex
  }
  
  int vc_counterexample_size(VC vc) {
@@ -1160,7 +1590,7 @@
    ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
  
    return ce->CounterExampleSize();
-@@ -1038,7 +1035,7 @@ Expr vc_bvConstExprFromInt(VC vc,
+@@ -941,7 +938,7 @@ Expr vc_bvConstExprFromInt(VC vc,
    bmstar b = (bmstar)(((stpstar)vc)->bm);
  
    unsigned long long int v = (unsigned long long int)value;
@@ -1169,7 +1599,7 @@
    //printf("%ull", max_n_bits);
    if(v > max_n_bits) {
      printf("CInterface: vc_bvConstExprFromInt: "\
-@@ -1581,16 +1578,11 @@ Expr vc_bvWriteToMemoryArray(VC vc,
+@@ -1484,16 +1481,11 @@ Expr vc_bvWriteToMemoryArray(VC vc,
      return vc_writeExpr(vc, array, byteIndex, element);
    else {
      int count = 1;
@@ -1186,7 +1616,7 @@
        low_elem = low_elem + 8;
        hi_elem = low_elem + 7;
              
-@@ -1765,7 +1757,6 @@ int vc_isBool(Expr e) {
+@@ -1668,7 +1660,6 @@ int vc_isBool(Expr e) {
  }
  
  void vc_Destroy(VC vc) {
@@ -1195,7 +1625,7 @@
    //    itend=created_exprs.end();it!=itend;it++) {
    //     BEEV::ASTNode * aaa = *it;
 --- ./src/printer/SMTLIB2Printer.cpp.orig	2010-07-10 08:49:13.000000000 -0600
-+++ ./src/printer/SMTLIB2Printer.cpp	2011-12-13 13:08:15.906474658 -0700
++++ ./src/printer/SMTLIB2Printer.cpp	2012-01-10 16:05:21.226609946 -0700
 @@ -210,7 +210,7 @@ void printVarDeclsToStream(ASTNodeSet& s
    		{
    			string close = "";
@@ -1206,7 +1636,7 @@
    				os << "(" << functionToSMTLIBName(kind,false);
    				os << " ";
 --- ./src/printer/SMTLIB1Printer.cpp.orig	2010-06-24 23:19:52.000000000 -0600
-+++ ./src/printer/SMTLIB1Printer.cpp	2011-12-13 13:08:15.906474658 -0700
++++ ./src/printer/SMTLIB1Printer.cpp	2012-01-10 16:05:21.226609946 -0700
 @@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod
    		{
    			string close = "";
@@ -1217,7 +1647,7 @@
    				os << "(" << functionToSMTLIBName(kind,true);
    				os << " ";
 --- ./src/printer/SMTLIBPrinter.h.orig	2010-05-23 20:03:46.000000000 -0600
-+++ ./src/printer/SMTLIBPrinter.h	2011-12-13 13:08:15.907474657 -0700
++++ ./src/printer/SMTLIBPrinter.h	2012-01-10 16:05:21.227609925 -0700
 @@ -24,7 +24,5 @@ namespace printer
  	ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1);
  
@@ -1226,8 +1656,8 @@
 -	static string tolower(const char * name);
  };
  #endif
---- ./src/sat/SimplifyingMinisat.h.orig	2011-06-22 20:17:24.000000000 -0600
-+++ ./src/sat/SimplifyingMinisat.h	2011-12-13 13:08:15.907474657 -0700
+--- ./src/sat/SimplifyingMinisat.h.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/SimplifyingMinisat.h	2012-01-10 16:05:21.227609925 -0700
 @@ -34,7 +34,7 @@ namespace BEEV
      bool
      simplify(); // Removes already satisfied clauses.
@@ -1237,19 +1667,19 @@
  
      virtual uint8_t modelValue(Var x) const;
  
---- ./src/sat/SATSolver.h.orig	2011-10-22 06:12:28.000000000 -0600
-+++ ./src/sat/SATSolver.h	2011-12-13 13:08:15.907474657 -0700
-@@ -58,7 +58,7 @@ namespace BEEV
-     virtual void setSeed(int i)
-     {}
+--- ./src/sat/SATSolver.h.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/SATSolver.h	2012-01-10 16:05:21.227609925 -0700
+@@ -61,7 +61,7 @@ namespace BEEV
+       exit(1);
+     }
  
 -    virtual int setVerbosity(int v) =0;
 +    virtual void setVerbosity(int v) =0;
  
      virtual lbool true_literal() =0;
      virtual lbool false_literal() =0;
---- ./src/sat/MinisatCore_prop.h.orig	2011-10-22 06:12:28.000000000 -0600
-+++ ./src/sat/MinisatCore_prop.h	2011-12-13 13:08:15.907474657 -0700
+--- ./src/sat/MinisatCore_prop.h.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/MinisatCore_prop.h	2012-01-10 16:05:21.227609925 -0700
 @@ -43,7 +43,7 @@ namespace BEEV
  
      virtual Var newVar();
@@ -1259,8 +1689,8 @@
  
      int nVars();
  
---- ./src/sat/SimplifyingMinisat.cpp.orig	2011-06-22 20:17:24.000000000 -0600
-+++ ./src/sat/SimplifyingMinisat.cpp	2011-12-13 13:08:15.908474656 -0700
+--- ./src/sat/SimplifyingMinisat.cpp.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/SimplifyingMinisat.cpp	2012-01-10 16:05:21.228609904 -0700
 @@ -17,7 +17,7 @@ namespace BEEV
    bool
    SimplifyingMinisat::addClause(const vec_literals& ps) // Add a clause to the solver.
@@ -1280,7 +1710,7 @@
      s->verbosity = v;
    }
 --- ./src/sat/cryptominisat2/Logger.cpp.orig	2010-06-04 12:11:26.000000000 -0600
-+++ ./src/sat/cryptominisat2/Logger.cpp	2011-12-13 13:08:15.908474656 -0700
++++ ./src/sat/cryptominisat2/Logger.cpp	2012-01-10 16:05:21.228609904 -0700
 @@ -372,8 +372,9 @@ void Logger::end(const finish_type finis
          fprintf(proof,"}\n");
          history.push_back(uniqueid);
@@ -1289,12 +1719,12 @@
 -        assert(proof == NULL);
 +        int err = fclose(proof);
 +        assert(err == 0);
-+	proof = NULL;
++        proof = NULL;
      }
  
      if (statistics_on) {
 --- ./src/sat/cryptominisat2/FailedVarSearcher.cpp.orig	2010-07-02 08:35:28.000000000 -0600
-+++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp	2011-12-13 13:08:15.909474655 -0700
++++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp	2012-01-10 16:05:21.229609884 -0700
 @@ -261,7 +261,6 @@ const bool FailedVarSearcher::search(uin
      }*/
  
@@ -1312,7 +1742,7 @@
              solver.clauseCleaner->removeAndCleanAll();
          }
 --- ./src/sat/CryptoMinisat.cpp.orig	2010-08-20 06:07:42.000000000 -0600
-+++ ./src/sat/CryptoMinisat.cpp	2011-12-13 13:08:15.909474655 -0700
++++ ./src/sat/CryptoMinisat.cpp	2012-01-10 16:05:21.230609864 -0700
 @@ -34,7 +34,7 @@ namespace BEEV
      for (int i =0; i<ps.size();i++)
        v.push(MINISAT::Lit(var(ps[i]), sign(ps[i])));
@@ -1332,7 +1762,7 @@
      s->verbosity = v;
    }
 --- ./src/sat/core_prop/Solver_prop.cc.orig	2011-11-27 19:55:18.000000000 -0700
-+++ ./src/sat/core_prop/Solver_prop.cc	2011-12-13 13:08:15.909474655 -0700
++++ ./src/sat/core_prop/Solver_prop.cc	2012-01-10 16:05:21.230609864 -0700
 @@ -171,11 +171,11 @@ Solver_prop::addArray(int array_id, cons
  
      if (!ok) return false;
@@ -1356,7 +1786,7 @@
                  assert(ca[confl][0] ==p);
                  assert(value(p) != l_Undef);
 --- ./src/sat/core_prop/Solver_prop.h.orig	2011-11-27 19:55:18.000000000 -0700
-+++ ./src/sat/core_prop/Solver_prop.h	2011-12-13 13:08:15.910474654 -0700
++++ ./src/sat/core_prop/Solver_prop.h	2012-01-10 16:05:21.231609844 -0700
 @@ -36,8 +36,10 @@ namespace Minisat {
      typedef unsigned int uint128_t __attribute__((mode(TI)));
      static inline uint32_t hash(uint128_t x){ return (uint32_t)x; }
@@ -1378,7 +1808,7 @@
                  printf("Array ID:%d\n", array_id);
                  printf("------------\n");
 --- ./src/sat/utils/Options.h.orig	2010-11-27 19:45:43.000000000 -0700
-+++ ./src/sat/utils/Options.h	2011-12-13 13:08:15.911474653 -0700
++++ ./src/sat/utils/Options.h	2012-01-10 16:05:21.231609844 -0700
 @@ -60,7 +60,7 @@ class Option
      struct OptionLt {
          bool operator()(const Option* x, const Option* y) {
@@ -1388,8 +1818,8 @@
          }
      };
  
---- ./src/sat/MinisatCore.cpp.orig	2011-10-22 06:12:28.000000000 -0600
-+++ ./src/sat/MinisatCore.cpp	2011-12-13 13:08:15.911474653 -0700
+--- ./src/sat/MinisatCore.cpp.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/MinisatCore.cpp	2012-01-10 16:05:21.231609844 -0700
 @@ -22,7 +22,7 @@ namespace BEEV
    bool
    MinisatCore<T>::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver.
@@ -1408,8 +1838,8 @@
    {
      s->verbosity = v;
    }
---- ./src/sat/MinisatCore_prop.cpp.orig	2011-10-22 06:12:28.000000000 -0600
-+++ ./src/sat/MinisatCore_prop.cpp	2011-12-13 13:08:15.911474653 -0700
+--- ./src/sat/MinisatCore_prop.cpp.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/MinisatCore_prop.cpp	2012-01-10 16:05:21.232609824 -0700
 @@ -30,7 +30,7 @@ namespace BEEV
    bool
    MinisatCore_prop<T>::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver.
@@ -1428,8 +1858,8 @@
    {
      s->verbosity = v;
    }
---- ./src/sat/CryptoMinisat.h.orig	2010-08-20 06:07:42.000000000 -0600
-+++ ./src/sat/CryptoMinisat.h	2011-12-13 13:08:15.912474651 -0700
+--- ./src/sat/CryptoMinisat.h.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/CryptoMinisat.h	2012-01-10 16:05:21.232609824 -0700
 @@ -36,7 +36,7 @@ namespace BEEV
  
      virtual Var newVar();
@@ -1439,8 +1869,8 @@
  
      int nVars();
  
---- ./src/sat/MinisatCore.h.orig	2010-08-20 06:07:42.000000000 -0600
-+++ ./src/sat/MinisatCore.h	2011-12-13 13:08:15.912474651 -0700
+--- ./src/sat/MinisatCore.h.orig	2012-01-09 21:59:09.000000000 -0700
++++ ./src/sat/MinisatCore.h	2012-01-10 16:05:21.232609824 -0700
 @@ -40,7 +40,7 @@ namespace BEEV
  
      virtual Var newVar();
@@ -1451,7 +1881,7 @@
      int nVars();
  
 --- ./src/extlib-abc/kit.h.orig	2011-02-09 18:31:59.000000000 -0700
-+++ ./src/extlib-abc/kit.h	2011-12-13 13:08:15.912474651 -0700
++++ ./src/extlib-abc/kit.h	2012-01-10 16:05:21.232609824 -0700
 @@ -53,11 +53,15 @@ struct Kit_Sop_t_
      unsigned *        pCubes;         // the storage for cubes
  };
@@ -1464,8 +1894,8 @@
 -    unsigned          fCompl   :  1;   // the complemented bit
 -    unsigned          Node     : 30;   // the decomposition node pointed by the edge
 +    struct {
-+         unsigned     fCompl   :  1;   // the complemented bit
-+         unsigned     Node     : 30;   // the decomposition node pointed by the edge
++        unsigned          fCompl   :  1;   // the complemented bit
++        unsigned          Node     : 30;   // the decomposition node pointed by the edge
 +    } edgeBits;
 +
 +    unsigned int      edgeInt;
@@ -1505,14 +1935,14 @@
  static inline int          Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode )   { return pNode - pGraph->pNodes;                      }
  static inline int          Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
 -static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )                           { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.Node );      }
-+static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )                           { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node );      }
++static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )                           { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node ); }
  static inline int          Kit_GraphVarInt( Kit_Graph_t * pGraph )                        { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
 -static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node);     }
 -static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node);     }
 -static inline int          Kit_GraphRootLevel( Kit_Graph_t * pGraph )                     { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level;                                        }
-+static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node);     }
-+static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node);     }
-+static inline int          Kit_GraphRootLevel( Kit_Graph_t * pGraph )                     { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level;                                        }
++static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node); }
++static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node); }
++static inline int          Kit_GraphRootLevel( Kit_Graph_t * pGraph )                     { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level;                               }
  
 -static inline int          Kit_Float2Int( float Val )     { return *((int *)&Val);               }
 -static inline float        Kit_Int2Float( int Num )       { return *((float *)&Num);             }
@@ -1539,7 +1969,7 @@
  
  /*=== kitBdd.c ==========================================================*/
 --- ./src/extlib-abc/aig/kit/kitSop.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/kit/kitSop.c	2011-12-13 13:08:15.913474649 -0700
++++ ./src/extlib-abc/aig/kit/kitSop.c	2012-01-10 16:05:21.233609804 -0700
 @@ -174,7 +174,7 @@ void Kit_SopDivideByCube( Kit_Sop_t * cS
  ***********************************************************************/
  void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
@@ -1550,7 +1980,7 @@
      assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
      // consider special case
 --- ./src/extlib-abc/aig/kit/kitAig.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/kit/kitAig.c	2011-12-13 13:08:15.913474649 -0700
++++ ./src/extlib-abc/aig/kit/kitAig.c	2012-01-10 16:05:21.233609804 -0700
 @@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_
      // build the AIG nodes corresponding to the AND gates of the graph
      Kit_GraphForEachNode( pGraph, pNode, i )
@@ -1563,7 +1993,7 @@
      }
      // complement the result if necessary
 --- ./src/extlib-abc/aig/kit/kitGraph.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/kit/kitGraph.c	2011-12-13 13:08:15.914474647 -0700
++++ ./src/extlib-abc/aig/kit/kitGraph.c	2012-01-10 16:05:21.234609784 -0700
 @@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0()
      pGraph = ALLOC( Kit_Graph_t, 1 );
      memset( pGraph, 0, sizeof(Kit_Graph_t) );
@@ -1689,7 +2119,7 @@
          pNode->pFunc = (void *)(long)uTruth;
      }
 --- ./src/extlib-abc/aig/aig/aigTable.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/aig/aigTable.c	2011-12-13 13:08:15.914474647 -0700
++++ ./src/extlib-abc/aig/aig/aigTable.c	2012-01-10 16:05:21.234609784 -0700
 @@ -74,8 +74,8 @@ void Aig_TableResize( Aig_Man_t * p )
  {
      Aig_Obj_t * pEntry, * pNext;
@@ -1702,7 +2132,7 @@
      pTableOld = p->pTable;
      nTableSizeOld = p->nTableSize;
 --- ./src/extlib-abc/aig/aig/aigShow.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/aig/aigShow.c	2011-12-13 13:08:15.914474647 -0700
++++ ./src/extlib-abc/aig/aig/aigShow.c	2012-01-10 16:05:21.234609784 -0700
 @@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan,
  void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
  {
@@ -1713,7 +2143,7 @@
      FILE * pFile;
      // create the file name
 --- ./src/extlib-abc/aig/aig/aigObj.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/aig/aigObj.c	2011-12-13 13:08:15.915474646 -0700
++++ ./src/extlib-abc/aig/aig/aigObj.c	2012-01-10 16:05:21.234609784 -0700
 @@ -299,8 +299,10 @@ void Aig_NodeFixBufferFanins( Aig_Man_t
          pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) );
  //    else if ( Aig_ObjIsLatch(pObj) )
@@ -1727,7 +2157,7 @@
      Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel );
  }
 --- ./src/extlib-abc/aig/cnf/cnfWrite.c.orig	2011-01-07 21:23:57.000000000 -0700
-+++ ./src/extlib-abc/aig/cnf/cnfWrite.c	2011-12-13 13:08:15.915474646 -0700
++++ ./src/extlib-abc/aig/cnf/cnfWrite.c	2012-01-10 16:05:21.235609764 -0700
 @@ -352,7 +352,6 @@ Cnf_Dat_t * Cnf_DeriveSimple_Additional(
      int Number = old->nVars+1;
  
@@ -1737,7 +2167,7 @@
      	if (pCnf->pVarNums[pObj->Id] == -1) // new!
      		pCnf->pVarNums[pObj->Id] = Number++;
 --- ./src/extlib-abc/aig/dar/darPrec.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/dar/darPrec.c	2011-12-13 13:08:15.915474646 -0700
++++ ./src/extlib-abc/aig/dar/darPrec.c	2012-01-10 16:05:21.235609764 -0700
 @@ -258,11 +258,9 @@ unsigned Dar_TruthPolarize( unsigned uTr
          0xFF00FF00,    // 1111 1111 0000 0000 1111 1111 0000 0000
          0xFFFF0000     // 1111 1111 1111 1111 0000 0000 0000 0000
@@ -1753,7 +2183,7 @@
          if ( Polarity & (1 << v) )
          {
 --- ./src/extlib-abc/aig/dar/darRefact.c.orig	2010-03-06 06:48:41.000000000 -0700
-+++ ./src/extlib-abc/aig/dar/darRefact.c	2011-12-13 13:08:15.916474646 -0700
++++ ./src/extlib-abc/aig/dar/darRefact.c	2012-01-10 16:05:21.236609744 -0700
 @@ -213,7 +213,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
  {
      Kit_Node_t * pNode, * pNode0, * pNode1;
@@ -1784,16 +2214,16 @@
              pAnd  = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
              // return -1 if the node is the same as the original root
              if ( Aig_Regular(pAnd) == pRoot )
-@@ -263,8 +263,6 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
+@@ -263,7 +263,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
                  LevelNew = (int)Aig_Regular(pAnd0)->Level;
              else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) )
                  LevelNew = (int)Aig_Regular(pAnd1)->Level;
 -            LevelOld = (int)Aig_Regular(pAnd)->Level;
--//            assert( LevelNew == LevelOld );
++//            LevelOld = (int)Aig_Regular(pAnd)->Level;
+ //            assert( LevelNew == LevelOld );
          }
          if ( LevelNew > LevelMax )
-             return -1;
-@@ -312,8 +310,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Ma
+@@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Ma
  //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
      Kit_GraphForEachNode( pGraph, pNode, i )
      {
@@ -1804,19 +2234,19 @@
          pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
  /*
  printf( "Checking " );
---- ./src/AST/ASTmisc.cpp.orig	2011-09-12 08:58:35.000000000 -0600
-+++ ./src/AST/ASTmisc.cpp	2011-12-13 13:08:15.916474646 -0700
-@@ -76,7 +76,7 @@ bool containsArrayOps(const ASTNode& n,
+--- ./src/AST/ASTmisc.cpp.orig	2012-01-09 22:53:22.000000000 -0700
++++ ./src/AST/ASTmisc.cpp	2012-01-10 16:05:21.236609744 -0700
+@@ -150,7 +150,7 @@ namespace BEEV
  
-         visited.insert(n.GetNodeNum());
+     visited.insert(n.GetNodeNum());
  
--	for (int i =0; i < n.Degree();i++)
-+	for (size_t i =0; i < n.Degree();i++)
- 		if (containsArrayOps(n[i],visited))
- 			return true;
+-    for (int i = 0; i < n.Degree(); i++)
++    for (size_t i = 0; i < n.Degree(); i++)
+       numberOfReadsLessThan(n[i], visited, soFar,limit);
+   }
  
---- ./src/AST/ArrayTransformer.cpp.orig	2011-09-12 08:58:35.000000000 -0600
-+++ ./src/AST/ArrayTransformer.cpp	2011-12-13 13:08:15.916474646 -0700
+--- ./src/AST/ArrayTransformer.cpp.orig	2011-12-28 19:00:01.000000000 -0700
++++ ./src/AST/ArrayTransformer.cpp	2012-01-10 16:05:21.236609744 -0700
 @@ -61,7 +61,6 @@ namespace BEEV
  			   iset_end = arrayToIndexToRead.end();
  			 iset != iset_end; iset++)
@@ -1825,108 +2255,101 @@
  				map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
  
  				for (map<ASTNode, ArrayTransformer::ArrayRead>::iterator it =mapper.begin() ; it != mapper.end();it++)
---- ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig	2011-11-30 06:57:18.000000000 -0700
-+++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp	2011-12-13 13:08:15.917474646 -0700
-@@ -369,7 +369,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
- 	const ASTNode& in2 = swap ? children[0] : children[1];
- 	const Kind k1 = in1.GetKind();
- 	const Kind k2 = in2.GetKind();
--	const int width = in1.GetValueWidth();
-+	const unsigned int width = in1.GetValueWidth();
+--- ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig	2012-01-09 20:39:36.000000000 -0700
++++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp	2012-01-10 16:05:21.237609723 -0700
+@@ -384,7 +384,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c
+   const ASTNode& in2 = swap ? children[0] : children[1];
+   const Kind k1 = in1.GetKind();
+   const Kind k2 = in2.GetKind();
+-  const int width = in1.GetValueWidth();
++  const unsigned int width = in1.GetValueWidth();
  
- 	if (in1 == in2)
- 		//terms are syntactically the same
-@@ -386,7 +386,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
-         if ((k1 == BEEV::BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BEEV::BVNEG && k2 == BEEV::BVCONST))
-           return NodeFactory::CreateNode(BEEV::EQ, in1[0], NodeFactory::CreateTerm(k1,width, in2 ));
+   if (in1 == in2)
+     //terms are syntactically the same
+@@ -401,7 +401,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c
+   if ((k1 == BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BVNEG && k2 == BEEV::BVCONST))
+     return NodeFactory::CreateNode(EQ, in1[0], NodeFactory::CreateTerm(k1, width, in2));
  
--        if (k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
-+        if ((k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST) || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
-           return NodeFactory::CreateNode(BEEV::EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 ));
+-  if (k2 == BVUMINUS && k1 == BEEV::BVCONST || (k2 == BVNEG && k1 == BEEV::BVCONST))
++  if ((k2 == BVUMINUS && k1 == BEEV::BVCONST) || (k2 == BVNEG && k1 == BEEV::BVCONST))
+     return NodeFactory::CreateNode(EQ, in2[0], NodeFactory::CreateTerm(k2, width, in1));
  
-         if ((k1 == BEEV::BVNEG && in1[0] == in2) || (k2 == BEEV::BVNEG && in2[0] == in1))
-@@ -449,13 +449,13 @@ ASTNode SimplifyingNodeFactory::CreateSi
- 	      {
- 	         int match1 =-1, match2=-1;
+   if ((k1 == BVNEG && in1[0] == in2) || (k2 == BVNEG && in2[0] == in1))
+@@ -460,8 +460,8 @@ SimplifyingNodeFactory::CreateSimpleEQ(c
+         {
+           int match1 = -1, match2 = -1;
  
--	        for (int i =0; i < c1.size();i++)
--	            for (int j =0; j < c2.size();j++)
-+	        for (size_t i =0; i < c1.size();i++)
-+	            for (size_t j =0; j < c2.size();j++)
- 	              {
- 	                if (c1[i] == c2[j])
- 	                  {
--	                    match1 = i;
--	                    match2 = j;
-+	                    match1 = (int)i;
-+	                    match2 = (int)j;
- 	                  }
- 	              }
+-          for (int i = 0; i < c1.size(); i++)
+-            for (int j = 0; j < c2.size(); j++)
++          for (int i = 0; (size_t)i < c1.size(); i++)
++            for (int j = 0; (size_t)j < c2.size(); j++)
+               {
+                 if (c1[i] == c2[j])
+                   {
+@@ -519,7 +519,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c
+       bool foundZero = false, foundOne = false;
+       const unsigned original_width = in2[0].GetValueWidth();
+       const unsigned new_width = in2.GetValueWidth();
+-      for (int i = original_width - 1; i < new_width; i++)
++      for (unsigned int i = original_width - 1; i < new_width; i++)
+         if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i))
+           foundOne = true;
+         else
+@@ -1103,7 +1103,7 @@ SimplifyingNodeFactory::CreateTerm(Kind
+       bool oneFound = false;
+       bool zeroFound = false;
  
-@@ -510,7 +510,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
-               bool foundZero=false, foundOne=false;
-               const unsigned original_width = in2[0].GetValueWidth();
-               const unsigned new_width = in2.GetValueWidth();
--              for (int i = original_width-1; i < new_width;i++)
-+              for (unsigned i = original_width-1; i < new_width;i++)
-                       if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i))
-                               foundOne=true;
-                       else
-@@ -1044,7 +1044,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
- 	    bool oneFound=false;
- 	    bool zeroFound=false;
- 
--	    for (int i = 0; i < children.size(); i++)
-+	    for (size_t i = 0; i < children.size(); i++)
+-      for (int i = 0; i < children.size(); i++)
++      for (size_t i = 0; i < children.size(); i++)
+         {
+           if (children[i].GetKind() == BEEV::BVCONST)
              {
-               if (children[i].GetKind() == BEEV::BVCONST)
-                 {
-@@ -1063,7 +1063,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
- 	    else if (oneFound)
- 	      {
- 	        ASTVec new_children;
--                for (int i = 0; i < children.size(); i++)
-+                for (size_t i = 0; i < children.size(); i++)
-                 {
-                   if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
-                     new_children.push_back(children[i]);
-@@ -1103,13 +1103,14 @@ ASTNode SimplifyingNodeFactory::CreateTe
- 	      int end=-1;
- 	      BEEV::CBV c = c0.GetBVConst();
- 	      bool bad= false;
--	      for (int i =0; i < width; i++)
-+	      for (unsigned i =0; i < width; i++)
- 	        {
--	          if (CONSTANTBV::BitVector_bit_test(c,i))
-+	          if (CONSTANTBV::BitVector_bit_test(c,i)) {
- 	            if (start == -1)
- 	                start = i; // first one bit.
- 	            else if (end != -1)
- 	              bad = true;
-+	          }
+@@ -1122,7 +1122,7 @@ SimplifyingNodeFactory::CreateTerm(Kind
+       else if (oneFound)
+         {
+           ASTVec new_children;
+-          for (int i = 0; i < children.size(); i++)
++          for (size_t i = 0; i < children.size(); i++)
+             {
+               if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
+                 new_children.push_back(children[i]);
+@@ -1162,13 +1162,14 @@ SimplifyingNodeFactory::CreateTerm(Kind
+         int end = -1;
+         BEEV::CBV c = c0.GetBVConst();
+         bool bad = false;
+-        for (int i = 0; i < width; i++)
++        for (unsigned int i = 0; i < width; i++)
+           {
+-            if (CONSTANTBV::BitVector_bit_test(c, i))
++            if (CONSTANTBV::BitVector_bit_test(c, i)) {
+               if (start == -1)
+                 start = i; // first one bit.
+               else if (end != -1)
+                 bad = true;
++            }
  
- 	          if (!CONSTANTBV::BitVector_bit_test(c,i))
- 	            if (start != -1 && end==-1)
-@@ -1129,7 +1130,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
-                       ASTNode z = bm.CreateZeroConst(start);
-                       result = NodeFactory::CreateTerm(BEEV::BVCONCAT, end+1, result,z);
-                     }
--                  if (end < width-1)
-+                  if (end < (int)width-1)
-                     {
-                       ASTNode z = bm.CreateZeroConst(width-end-1);
-                       result = NodeFactory::CreateTerm(BEEV::BVCONCAT, width, z,result);
-@@ -1190,7 +1191,6 @@ ASTNode SimplifyingNodeFactory::CreateTe
-               const unsigned outerHigh = children[1].GetUnsignedConst();
+             if (!CONSTANTBV::BitVector_bit_test(c, i))
+               if (start != -1 && end == -1)
+@@ -1189,7 +1190,7 @@ SimplifyingNodeFactory::CreateTerm(Kind
+                 ASTNode z = bm.CreateZeroConst(start);
+                 result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z);
+               }
+-            if (end < width - 1)
++            if (end < (int)width - 1)
+               {
+                 ASTNode z = bm.CreateZeroConst(width - end - 1);
+                 result = NodeFactory::CreateTerm(BVCONCAT, width, z, result);
+@@ -1252,7 +1253,6 @@ SimplifyingNodeFactory::CreateTerm(Kind
+         const unsigned outerHigh = children[1].GetUnsignedConst();
  
-               const unsigned innerLow = children[0][2].GetUnsignedConst();
--              const unsigned innerHigh = children[0][1].GetUnsignedConst();
-               result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh
-                   + innerLow), bm.CreateBVConst(32, outerLow + innerLow));
-             }
---- ./src/STPManager/STP.cpp.orig	2011-11-27 22:33:34.000000000 -0700
-+++ ./src/STPManager/STP.cpp	2011-12-13 13:08:15.917474646 -0700
-@@ -61,8 +61,8 @@ namespace BEEV {
+         const unsigned innerLow = children[0][2].GetUnsignedConst();
+-        const unsigned innerHigh = children[0][1].GetUnsignedConst();
+         result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh + innerLow),
+             bm.CreateBVConst(32, outerLow + innerLow));
+       }
+--- ./src/STPManager/STP.cpp.orig	2012-01-09 22:38:16.000000000 -0700
++++ ./src/STPManager/STP.cpp	2012-01-10 16:05:21.237609723 -0700
+@@ -59,8 +59,8 @@ namespace BEEV {
        newS = new MinisatCore<Minisat::Solver>();
      else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS)
        newS = new MinisatCore_prop<Minisat::Solver_prop>();
@@ -1938,7 +2361,7 @@
      SATSolver& NewSolver = *newS;
  
 --- ./src/parser/ParserInterface.h.orig	2011-07-09 00:56:51.000000000 -0600
-+++ ./src/parser/ParserInterface.h	2011-12-13 13:08:15.918474645 -0700
++++ ./src/parser/ParserInterface.h	2012-01-10 16:05:21.238609702 -0700
 @@ -214,7 +214,7 @@ public:
            assert(symbols.size() == cache.size());
            cache.erase(cache.end()-1);
diff --git a/stp.spec b/stp.spec
index 4255001..5fed360 100644
--- a/stp.spec
+++ b/stp.spec
@@ -1,11 +1,11 @@
 # Upstream occasionally releases a subversion snapshot, but no "regular"
 # releases since the 0.1 release.
-%global svnver 1434
-%global svntim 20111130svn
+%global svnver 1493
+%global svntim 20120109svn
 
 Name:		stp
 Version:	0.1
-Release:	7.%{svntim}%{?dist}
+Release:	8.%{svntim}%{?dist}
 Summary:	Constraint solver/decision procedure
 
 Group:		Applications/Engineering
@@ -50,7 +50,7 @@ Additional information can be found at:
 %package devel
 Summary:	Development files for STP constraint solver/decision procedure
 Group:		Applications/Engineering
-Requires:	%{name} = %{version}-%{release}
+Requires:	%{name}%{?_isa} = %{version}-%{release}
 Provides:	%{name}-static = %{version}-%{release}
 # This "devel" package provides a static (not dynamic) library because:
 # 1. This is the normal usage mode when linking this as a library;
@@ -109,6 +109,9 @@ make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir}
 %{_includedir}/stp/
 
 %changelog
+* Tue Jan 10 2012 Jerry James <loganjerry@gmail.com> - 0.1-8.20120109svn
+- Update to recent subversion snapshot
+
 * Tue Dec 13 2011 Jerry James <loganjerry@gmail.com> - 0.1-7.20111130svn
 - Update to recent subversion snapshot
 - Minor spec file cleanups