stp/stp-warning.patch

--- ./src/simplifier/UseITEContext.h.orig	2011-04-07 07:38:52.000000000 -0600
+++ ./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)
         {
           ASTVec flat = FlattenKind(OR, n[0].GetChildren());
-          for (int i = 0; i < flat.size(); i++)
+          for (size_t i = 0; i < flat.size(); i++)
             context.insert(nf->CreateNode(NOT, flat[i]));
         }
       else if (n.GetKind() == AND)
@@ -85,7 +85,7 @@ namespace BEEV
         }
       else
         {
-          for (int i = 0; i < n.GetChildren().size(); i++)
+          for (size_t i = 0; i < n.GetChildren().size(); i++)
             new_children.push_back(visit(n[i], visited, visited_empty, context));
         }
 
--- ./src/simplifier/AlwaysTrue.h.orig	2011-05-01 06:48:53.000000000 -0600
+++ ./src/simplifier/AlwaysTrue.h	2012-01-10 16:05:21.202610431 -0700
@@ -88,7 +88,7 @@ public:
     else
       new_state = state;
 
-    for (int i=0; i < n.Degree(); i++)
+    for (size_t i=0; i < n.Degree(); i++)
       {
         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	2012-01-10 16:05:21.210610269 -0700
@@ -46,12 +46,12 @@ public:
       vector<MutableASTNode *> tempChildren;
       tempChildren.reserve(n.Degree());
 
-      for (int i = 0; i < n.Degree(); i++)
+      for (size_t i = 0; i < n.Degree(); i++)
         tempChildren.push_back(build(n[i], visited));
 
       MutableASTNode * mut = createNode(n);
 
-      for (int i = 0; i < n.Degree(); i++)
+      for (size_t i = 0; i < n.Degree(); i++)
         tempChildren[i]->parents.insert(mut);
 
       mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end());
@@ -86,7 +86,7 @@ private:
         	assert(found);
         }
 
-        for (int i = 0; i < children.size(); i++)
+        for (size_t i = 0; i < children.size(); i++)
         {
         	// call check on all the children.
         	children[i]->checkInvariant();
@@ -116,7 +116,7 @@ private:
         return n;
 
       ASTVec newChildren;
-      for (int i = 0; i < children.size(); i++)
+      for (size_t i = 0; i < children.size(); i++)
         newChildren.push_back(children[i]->toASTNode(nf));
 
       // Don't use the hashing node factory here. Imagine CreateNode simplified down,
@@ -189,7 +189,7 @@ private:
       removeChildren(vars); // ignore the result
       children.clear();
       children.insert(children.begin(), newN->children.begin(), newN->children.end());
-      for (int i = 0; i < children.size(); i++)
+      for (size_t i = 0; i < children.size(); i++)
     	  children[i]->parents.insert(this);
 
       propagateUpDirty();
@@ -249,7 +249,7 @@ private:
 
           ASTNode& node = all[i]->n;
           bool found[node.GetValueWidth()];
-          for (int j=0; j <node.GetValueWidth();j++)
+          for (unsigned int j=0; j <node.GetValueWidth();j++)
             found[j] = false;
 
           ParentsType::const_iterator it;
@@ -330,7 +330,7 @@ private:
     static void
     cleanup()
     {
-      for (int i = 0; i < all.size(); i++)
+      for (size_t i = 0; i < all.size(); i++)
         delete all[i];
       all.clear();
     }
--- ./src/simplifier/EstablishIntervals.h.orig	2011-08-08 23:15:54.000000000 -0600
+++ ./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());
 
-      for (int i =0; i < result.Degree();i++)
+      for (size_t i =0; i < result.Degree();i++)
         new_children.push_back(replace(result[i],fromTo,cache));
 
       if (new_children == result.GetChildren())
@@ -496,7 +496,7 @@ namespace BEEV
               result = freshUnsignedInterval(n.GetValueWidth());
 
               // Copy in the minimum and maximum.
-        	  for (int i=0; i < n[0].GetValueWidth();i++)
+        	  for (unsigned int i=0; i < n[0].GetValueWidth();i++)
         	  {
         		  if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i))
         			  CONSTANTBV::BitVector_Bit_On(result->maxV,i);
@@ -509,7 +509,7 @@ namespace BEEV
         			  CONSTANTBV::BitVector_Bit_Off(result->minV,i);
         	  }
 
-        	  for (int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++)
+        	  for (unsigned int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++)
         		  CONSTANTBV::BitVector_Bit_Off(result->maxV,i);
     	  }
       } else if (knownC1)
@@ -517,13 +517,13 @@ namespace BEEV
           // Ignores what's already there for now..
 
           IntervalType * circ_result = freshUnsignedInterval(n.GetValueWidth());
-          for (int i=0; i < n[0].GetValueWidth()-1;i++)
+          for (unsigned int i=0; i < n[0].GetValueWidth()-1;i++)
           {
               CONSTANTBV::BitVector_Bit_On(circ_result->maxV,i);
               CONSTANTBV::BitVector_Bit_Off(circ_result->minV,i);
           }
 
-          for (int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++)
+          for (unsigned int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++)
           {
               CONSTANTBV::BitVector_Bit_Off(circ_result->maxV,i);
               CONSTANTBV::BitVector_Bit_On(circ_result->minV,i);
@@ -598,7 +598,7 @@ namespace BEEV
           CONSTANTBV::BitVector_increment(result->maxV);
 
           bool bad= false;
-          for (int i =0; i < children.size(); i++)
+          for (size_t i =0; i < children.size(); i++)
             {
               if (children[i] == NULL)
                 {
@@ -611,10 +611,10 @@ namespace BEEV
               e = CONSTANTBV::BitVector_Multiply(max, result->maxV, children[i]->maxV);
               assert (0 == e);
 
-              if (CONSTANTBV::Set_Max(max) >= width)
+              if (CONSTANTBV::Set_Max(max) >= (long)width)
                 bad = true;
 
-              for (int j = width; j < 2 * width; j++)
+              for (unsigned int j = width; j < 2 * width; j++)
                 {
                   if (CONSTANTBV::BitVector_bit_test(min, j))
                     bad = true;
@@ -687,7 +687,7 @@ namespace BEEV
 
           bool carry = false;
 
-          for (int i =0; i < children.size(); i++)
+          for (size_t i =0; i < children.size(); i++)
             {
               if (children[i] == NULL)
                 {
@@ -716,7 +716,7 @@ namespace BEEV
           if (knownC1)
           {
         	  // Copy in the minimum and maximum.
-        	  for (int i=0; i < n[1].GetValueWidth();i++)
+        	  for (unsigned int i=0; i < n[1].GetValueWidth();i++)
         	  {
         		  if (CONSTANTBV::BitVector_bit_test(children[1]->maxV,i))
         			  CONSTANTBV::BitVector_Bit_On(result->maxV,i);
@@ -733,7 +733,7 @@ namespace BEEV
           if (knownC0)
           {
         	  // Copy in the minimum and maximum.
-        	  for (int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++)
+        	  for (unsigned int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++)
         	  {
         		  if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i- n[1].GetValueWidth()))
         			  CONSTANTBV::BitVector_Bit_On(result->maxV,i);
@@ -754,7 +754,7 @@ namespace BEEV
 
     	  bool nonNull = true;
     	  // If all the children are known, output 'em.
-    	  for (int i=0; i < n.Degree();i++)
+    	  for (size_t i=0; i < n.Degree();i++)
     	  {
     		  if (children[i]== NULL)
     			  nonNull=false;
@@ -763,7 +763,7 @@ namespace BEEV
     	  if (false && nonNull && n.GetKind() != SYMBOL && n.GetKind() != AND)
     	  {
     	      cerr << n;
-    	      for (int i=0; i < n.Degree();i++)
+    	      for (size_t i=0; i < n.Degree();i++)
     	        children[i]->print();
     	  }
       }
@@ -796,10 +796,10 @@ namespace BEEV
 
     ~EstablishIntervals()
     {
-      for (int i =0; i < toDeleteLater.size();i++)
+      for (size_t i =0; i < toDeleteLater.size();i++)
         delete toDeleteLater[i];
 
-      for (int i =0; i < likeAutoPtr.size();i++)
+      for (size_t i =0; i < likeAutoPtr.size();i++)
         CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]);
 
       likeAutoPtr.clear();
--- ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp.orig	2010-11-27 20:45:32.000000000 -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;
 
-	Result result = NO_CHANGE;
-
 	FixedBits& op = *children[0];
 	FixedBits& shift = *children[1];
 
@@ -393,7 +391,6 @@ Result bvArithmeticRightShiftBothWays(ve
 			{
 				shift.setFixed(i, true);
 				shift.setValue(i, setOfPossibleShifts.getValue(i));
-				result = CHANGED;
 			}
 			else if (shift.isFixed(i) && shift.getValue(i)
 					!= setOfPossibleShifts.getValue(i))
@@ -550,7 +547,6 @@ Result bvArithmeticRightShiftBothWays(ve
 				{
 					output.setFixed(column, true);
 					output.setValue(column, allFixedTo);
-					result = CHANGED;
 				}
 			}
 		}
@@ -563,8 +559,6 @@ Result bvLeftShiftBothWays(vector<FixedB
 	assert(2== children.size());
 	assert(bitWidth > 0);
 
-	Result result = NO_CHANGE;
-
 	FixedBits& op = *children[0];
 	FixedBits& shift = *children[1];
 
@@ -761,7 +755,6 @@ Result bvLeftShiftBothWays(vector<FixedB
 			{
 				shift.setFixed(i, true);
 				shift.setValue(i, v.getValue(i));
-				result = CHANGED;
 			}
 			else if (shift.isFixed(i) && shift.getValue(i) != v.getValue(i))
 				return CONFLICT;
@@ -899,7 +892,6 @@ Result bvLeftShiftBothWays(vector<FixedB
 			{
 				output.setFixed(column, true);
 				output.setValue(column, allFixedTo);
-				result = CHANGED;
 			}
 		}
 	}
--- ./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)
     {
-      for (int i = 0; i < n.Degree(); i++)
+      for (size_t i = 0; i < n.Degree(); i++)
         workList->push(n[i]);
     }
 
@@ -462,7 +462,7 @@ namespace simplifier
 
       assert(FixedBits::equals(newBits, current));
 
-      for (int i = 0; i < n.Degree(); i++)
+      for (size_t i = 0; i < n.Degree(); i++)
         {
           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	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)
 {
-	Result r = NO_CHANGE;
-
 	assert(c0.getWidth() == c1.getWidth());
 
 	CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
@@ -135,7 +133,6 @@ Result bvSignedLessThanBothWays(FixedBit
 		{
 			output.setFixed(0, true);
 			output.setValue(0, true);
-			r = CHANGED;
 		}
 	}
 
@@ -153,7 +150,6 @@ Result bvSignedLessThanBothWays(FixedBit
 		{
 			output.setFixed(0, true);
 			output.setValue(0, false);
-			r = CHANGED;
 		}
 	}
 
@@ -183,7 +179,6 @@ Result bvSignedLessThanBothWays(FixedBit
 				c0.setFixed(msb, true);
 				c0.setValue(msb, true);
 				setSignedMinMax(c0, c0_min, c0_max);
-				r = CHANGED;
 			}
 			else
 			{
@@ -199,7 +194,6 @@ Result bvSignedLessThanBothWays(FixedBit
 				c1.setFixed(msb, true);
 				c1.setValue(msb, false);
 				setSignedMinMax(c1, c1_min, c1_max);
-				r = CHANGED;
 			}
 			else
 			{
@@ -222,7 +216,6 @@ Result bvSignedLessThanBothWays(FixedBit
 						c0.setFixed(i, true);
 						c0.setValue(i, false);
 						setSignedMinMax(c0, c0_min, c0_max);
-						r = CHANGED;
 					}
 					else
 					{
@@ -242,7 +235,6 @@ Result bvSignedLessThanBothWays(FixedBit
 						c1.setFixed(i, true);
 						c1.setValue(i, true);
 						setSignedMinMax(c1, c1_min, c1_max);
-						r = CHANGED;
 					}
 					else
 					{
@@ -259,8 +251,6 @@ Result bvSignedLessThanBothWays(FixedBit
 
 Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
 {
-	Result r = NO_CHANGE;
-
 	assert(c0.getWidth() == c1.getWidth());
 
 	CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
@@ -283,7 +273,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
 		{
 			output.setFixed(0, true);
 			output.setValue(0, true);
-			r = CHANGED;
 		}
 	}
 
@@ -299,7 +288,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
 		{
 			output.setFixed(0, true);
 			output.setValue(0, false);
-			r = CHANGED;
 		}
 	}
 
@@ -329,7 +317,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
 				c0.setFixed(msb, true);
 				c0.setValue(msb, true);
 				setSignedMinMax(c0, c0_min, c0_max);
-				r = CHANGED;
 			}
 			else
 			{
@@ -345,7 +332,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
 				c1.setFixed(msb, true);
 				c1.setValue(msb, false);
 				setSignedMinMax(c1, c1_min, c1_max);
-				r = CHANGED;
 			}
 			else
 			{
@@ -412,8 +398,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
 // UNSIGNED!!
 Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
 {
-	Result r = NO_CHANGE;
-
 	assert(c0.getWidth() == c1.getWidth());
 
 	CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
@@ -467,8 +451,6 @@ Result bvLessThanBothWays(FixedBits& c0,
 		return bvGreaterThanEqualsBothWays(c0, c1, t);
 	}
 
-	bool changed = false;
-
 	if (output.isFixed(0) && output.getValue(0))
 	{
 		// Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
@@ -484,7 +466,6 @@ Result bvLessThanBothWays(FixedBits& c0,
 					c0.setFixed(i, true);
 					c0.setValue(i, false);
 					setUnsignedMinMax(c0, c0_min, c0_max);
-					changed = true;
 				}
 				else
 				{
@@ -504,7 +485,6 @@ Result bvLessThanBothWays(FixedBits& c0,
 					c1.setFixed(i, true);
 					c1.setValue(i, true);
 					setUnsignedMinMax(c1, c1_min, c1_max);
-					changed = true;
 				}
 				else
 				{
@@ -521,8 +501,6 @@ Result bvLessThanBothWays(FixedBits& c0,
 
 Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
 {
-	Result r = NO_CHANGE;
-
 	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	2012-01-10 16:05:21.213610209 -0700
@@ -33,7 +33,6 @@ Result bvSubtractBothWays(vector<FixedBi
 	Addargs.push_back(&notB);
 	Addargs.push_back(&one);
 
-	bool changed = false;
 	while (true) // until it fixed points
 	{
 		Result result;
@@ -51,8 +50,6 @@ Result bvSubtractBothWays(vector<FixedBi
 
 		if (FixedBits::equals(initialNotB, notB) && FixedBits::equals(initialA, a) && FixedBits::equals(initialOut, output))
 			break;
-		else
-			changed = true;
 	}
 
 	return NOT_IMPLEMENTED;
@@ -214,8 +211,6 @@ void printArray(int f[], int width)
 
 Result bvAddBothWays(vector<FixedBits*>& children, FixedBits& output)
 {
-	Result result = NO_CHANGE;
-
 	const int bitWidth = output.getWidth();
 	const int numberOfChildren = children.size();
 
@@ -361,7 +356,6 @@ Result bvAddBothWays(vector<FixedBits*>&
 				{
 					output.setFixed(column, true);
 					output.setValue(column, newResult);
-					result = CHANGED;
 					changed = true;
 				}
 				else if (output.isFixed(column) && (output.getValue(column) != newResult))
--- ./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:
-      for (int i =0; i < n.Degree(); i ++)
+      for (size_t i =0; i < n.Degree(); i ++)
         build(n[i],polarity);
       break;
 
@@ -120,7 +120,7 @@ public:
 
     default:
         polarity = bothPolarity; // both
-        for (int i =0; i < n.Degree(); i ++)
+        for (size_t i =0; i < n.Degree(); i ++)
           build(n[i],polarity);
       break;
     }
--- ./src/simplifier/VariablesInExpression.cpp.orig	2011-02-01 05:41:57.000000000 -0700
+++ ./src/simplifier/VariablesInExpression.cpp	2012-01-10 16:05:21.214610188 -0700
@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbo
 	}
 
 	vector<Symbols*> children;
-	for (int i = 0; i < n.Degree(); i++) {
+	for (size_t i = 0; i < n.Degree(); i++) {
 		Symbols* v = getSymbol(n[i]);
 		if (!v->empty())
 			children.push_back(v);
@@ -111,7 +111,7 @@ ASTNodeSet * VariablesInExpression::Seto
 	vector<Symbols*> av;
 	VarSeenInTerm(symbol,visited,*symbols,av);
 
-	for (int i =0; i < av.size();i++)
+	for (size_t i =0; i < av.size();i++)
 	{
 		const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;
 		symbols->insert(sym.begin(), sym.end());
@@ -155,7 +155,7 @@ bool VariablesInExpression::VarSeenInTer
 		sort(av.begin(), av.end());
 
 		//cout << "===" << endl;
-		for (int i = 0; i < av.size(); i++) {
+		for (size_t i = 0; i < av.size(); i++) {
 			if (i!=0 && av[i] == av[i-1])
 				continue;
 
--- ./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());
-	for (int i =0; i < av.size();i++)
+	for (size_t i =0; i < av.size();i++)
 	{
 		if (i!=0 && av[i] == av[i-1])
 			continue; // Treat it like a set of Symbol* in effect.
--- ./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);
       }
 
-    for (int i = 0; i < n.Degree(); i++)
+    for (size_t i = 0; i < n.Degree(); i++)
       {
         checkIfInSimplifyMap(n[i], visited);
       }
@@ -516,6 +516,7 @@ namespace BEEV
       return getConstantBit(n[0], i);
 
     assert(false);
+    return -1;
   }
 
   ASTNode
@@ -1284,7 +1285,7 @@ namespace BEEV
     else
       {
         ASTVec newC;
-        for (int i = 0; i < a.GetChildren().size(); i++)
+        for (size_t i = 0; i < a.GetChildren().size(); i++)
           {
             newC.push_back(SimplifyFormula(a[i], false, VarConstMap));
           }
@@ -1646,9 +1647,9 @@ namespace BEEV
     assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
     const int inputValueWidth = output.GetValueWidth();
 
-    int lengthA = output.GetChildren()[0][0].GetValueWidth();
-    int lengthB = output.GetChildren()[1][0].GetValueWidth();
-    int maxLength;
+    unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth();
+    unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth();
+    unsigned int maxLength;
     if (BVMULT == output.GetKind())
       maxLength = lengthA + lengthB;
     else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
@@ -1676,7 +1677,7 @@ namespace BEEV
   {
     const ASTNode a = children[0];
     const ASTNode b = children[1];
-    const int width = children[0].GetValueWidth();
+    const unsigned int width = children[0].GetValueWidth();
     ASTNode output;
 
     assert(b.isConstant());
@@ -1707,7 +1708,7 @@ namespace BEEV
   {
     const ASTNode a = children[0];
     const ASTNode b = children[1];
-    const int width = children[0].GetValueWidth();
+    const unsigned int width = children[0].GetValueWidth();
     ASTNode output;
 
     assert(b.isConstant());
@@ -1888,7 +1889,7 @@ namespace BEEV
     //I haven't measured if this is worth the expense.
       {
         bool notSimplified = false;
-        for (int i = 0; i < inputterm.Degree(); i++)
+        for (size_t i = 0; i < inputterm.Degree(); i++)
           if (inputterm[i].GetType() != ARRAY_TYPE)
             if (!hasBeenSimplified(inputterm[i]))
               {
@@ -2229,7 +2230,6 @@ namespace BEEV
         case BVEXTRACT:
           {
             const unsigned innerLow = a0[2].GetUnsignedConst();
-            const unsigned innerHigh = a0[1].GetUnsignedConst();
 
             output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow),
                 _bm->CreateBVConst(32, j_val + innerLow));
@@ -2629,7 +2629,7 @@ namespace BEEV
             assert(BVTypeCheck(output));
 
             // If the leading bits are zero. Replace it by a concat with zero.
-            int i;
+            unsigned int i;
             if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0))
               {
                 // i contains the number of leading zeroes.
@@ -2651,13 +2651,13 @@ namespace BEEV
           }
         if (output.GetKind() == BVAND)
           {
-            int trailingZeroes = 0;
-            for (int i = 0; i < output.Degree(); i++)
+            unsigned int trailingZeroes = 0;
+            for (size_t i = 0; i < output.Degree(); i++)
               {
                 const ASTNode& n = output[i];
                 if (n.GetKind() != BVCONST)
                   continue;
-                int j;
+                unsigned int j;
                 for (j = 0; j < n.GetValueWidth(); j++)
                   if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j))
                     break;
@@ -2674,7 +2674,7 @@ namespace BEEV
                     //cerr << "old" << output;
                     ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes);
                     ASTVec newChildren;
-                    for (int i = 0; i < output.Degree(); i++)
+                    for (size_t i = 0; i < output.Degree(); i++)
                       newChildren.push_back(
                           nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i],
                               _bm->CreateBVConst(32, output.GetValueWidth() - 1),
--- ./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;
     children.reserve(number_of_children);
-    for (int i =0; i < number_of_children; i++)
+    for (unsigned int i =0; i < number_of_children; i++)
     {
     	if (input_children[i].isConstant())
     		children.push_back(input_children[i]);
--- ./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);
 
-	int substitutionsLastApplied;
+	size_t substitutionsLastApplied;
 public:
 
 	bool hasUnappliedSubstitutions()
--- ./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)
   {
-      for (int i =0; i < children.size(); i++)
+      for (size_t i =0; i < children.size(); i++)
         if (!children[i]->isUnconstrained())
           return false;
 
@@ -105,7 +105,7 @@ namespace BEEV
     // Going to be rebuilt later anyway, so discard.
     vector<MutableASTNode*> variables;
 
-    for (int i =0; i <extracts.size(); i++)
+    for (size_t i =0; i <extracts.size(); i++)
       {
         ASTNode& var = extracts[i]->n;
         assert(var.GetKind() == SYMBOL);
@@ -156,7 +156,7 @@ namespace BEEV
         }
 
     ASTNode concat = concatVec[0];
-    for (int i=1; i < concatVec.size();i++)
+    for (size_t i=1; i < concatVec.size();i++)
       {
           assert(!concat.IsNull());
           concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat);
@@ -189,7 +189,7 @@ namespace BEEV
 
     topMutable->getAllUnconstrainedVariables(variable_array);
 
-    for (int i =0; i < variable_array.size() ; i++)
+    for (size_t i =0; i < variable_array.size() ; i++)
       {
         // Don't make this is a reference. If the vector gets resized, it will point to
         // memory that no longer contains the object.
@@ -213,7 +213,7 @@ namespace BEEV
         //nb. The children might be dirty. i.e. not have substitutions written through them yet.
         ASTVec children;
         children.reserve(mutable_children.size());
-        for (int j = 0; j <mutable_children.size(); j++ )
+        for (size_t j = 0; j <mutable_children.size(); j++ )
           children.push_back(mutable_children[j]->n);
 
         const size_t numberOfChildren = children.size();
@@ -247,7 +247,7 @@ namespace BEEV
               {
                   int found = 0;
 
-                  for (int i = 0; i < numberOfChildren; i++)
+                  for (size_t i = 0; i < numberOfChildren; i++)
                     {
                       if (children[i] == var)
                         found++;
@@ -434,7 +434,7 @@ namespace BEEV
               {
                 ASTNodeSet already;
                 ASTNode v =replaceParentWithFresh(muteParent, variable_array);
-                for (int i =0; i < numberOfChildren;i++)
+                for (size_t i =0; i < numberOfChildren;i++)
                   {
                     /* to avoid problems with:
                     734:(AND
@@ -469,7 +469,7 @@ namespace BEEV
                 ASTNode v =replaceParentWithFresh(muteParent, variable_array);
 
                 ASTVec others;
-                for (int i = 0; i < numberOfChildren; i++)
+                for (size_t i = 0; i < numberOfChildren; i++)
                 {
                     if (children[i] !=var)
                         others.push_back(mutable_children[i]->toASTNode(nf));
@@ -622,7 +622,7 @@ namespace BEEV
         case BVPLUS:
               {
                 ASTVec other;
-                for (int i = 0; i < children.size(); i++)
+                for (size_t i = 0; i < children.size(); i++)
                   if (children[i] != var)
                     other.push_back(mutable_children[i]->toASTNode(nf));
 
@@ -644,7 +644,6 @@ namespace BEEV
               {
                 ASTNode v =replaceParentWithFresh(muteParent, variable_array);
 
-                const unsigned resultWidth = width;
                 const unsigned operandWidth = var.GetValueWidth();
                 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	2012-01-10 16:05:21.219610086 -0700
@@ -46,7 +46,7 @@ namespace BEEV
         assert(symbol.GetKind() == SYMBOL);
         vector<bool>  bitVector_array(symbolWidth,false);
 
-        for (int index = 0; index < v.size(); index++)
+        for (size_t index = 0; index < v.size(); index++)
           {
             const unsigned sat_variable_index = v[index];
 
@@ -863,7 +863,7 @@ namespace BEEV
       ASTNode symbol = it->first;
       vector<unsigned> v = it->second;
 
-      for (int i =0 ; i < v.size();i++)
+      for (size_t i =0 ; i < v.size();i++)
         {
         if (v[i] == ~((unsigned)0)) // nb. special value.
           continue;
--- ./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);
                 // It was ommitted from the initial problem, so assign it freshly.
-                for (int i = 0; i < a.GetValueWidth(); i++)
+                for (unsigned int i = 0; i < a.GetValueWidth(); i++)
                     {
                         SATSolver::Var v = SatSolver.newVar();
                         // We probably don't want the variable eliminated.
@@ -55,7 +55,7 @@ namespace BEEV
     getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar,
             Polarity polary = BOTH)
     {
-        const int width = a.GetValueWidth();
+        const unsigned int width = a.GetValueWidth();
         assert(width == b.GetValueWidth());
         assert(!a.isConstant() || !b.isConstant());
 
@@ -72,7 +72,7 @@ namespace BEEV
                 SATSolver::vec_literals all;
                 const int result = SatSolver.newVar();
 
-                for (int i = 0; i < width; i++)
+                for (unsigned int i = 0; i < width; i++)
                     {
                         SATSolver::vec_literals s;
 
@@ -116,7 +116,7 @@ namespace BEEV
                 }
                 return result;
             }
-        else if (v_a.size() == 0 ^ v_b.size() == 0)
+        else if ((v_a.size() == 0) ^ (v_b.size() == 0))
             {
                 ASTNode constant = a.isConstant() ? a : b;
                 vector<unsigned> vec = v_a.size() == 0 ? v_b : v_a;
@@ -128,7 +128,7 @@ namespace BEEV
                 all.push(SATSolver::mkLit(result, false));
 
                 CBV v = constant.GetBVConst();
-                for (int i = 0; i < width; i++)
+                for (unsigned int i = 0; i < width; i++)
                     {
                         if (polary != RIGHT_ONLY)
                             {
@@ -214,7 +214,7 @@ namespace BEEV
     void
     applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector<AxiomToBe> & toBe, SATSolver & SatSolver)
     {
-        for (int i = 0; i < toBe.size(); i++)
+        for (size_t i = 0; i < toBe.size(); i++)
             {
                 applyAxiomToSAT(SatSolver, toBe[i], satVar);
             }
@@ -269,7 +269,6 @@ namespace BEEV
         for (vector<pair<ASTNode, ArrayTransformer::arrTypeMap> >::const_iterator iset = arrayToIndex.begin(),
                 iset_end = arrayToIndex.end(); iset != iset_end; iset++)
             {
-                const ASTNode& ArrName = iset->first;
                 const map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
 
                 vector<ASTNode> listOfIndices;
@@ -318,13 +317,13 @@ namespace BEEV
 
                 //loop over the list of indices for the array and create LA,
                 //and add to inputAlreadyInSAT
-                for (int i = 0; i < listOfIndices.size(); i++)
+                for (size_t i = 0; i < listOfIndices.size(); i++)
                     {
                         const ASTNode& index_i = listOfIndices[i];
                         const Kind iKind = index_i.GetKind();
 
                         // Create all distinct pairs of indexes.
-                        for (int j = i + 1; j < listOfIndices.size(); j++)
+                        for (size_t j = i + 1; j < listOfIndices.size(); j++)
                             {
                                 const ASTNode& index_j = listOfIndices[j];
 
--- ./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.
         // For boolean we create a vector of size 1.
-        if (n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
+        if ((n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
           {
             const ASTNode& symbol = n.GetKind() == BVGETBIT ? n[0] : n;
             const unsigned index = n.GetKind() == BVGETBIT ? n[1].GetUnsignedConst() : 0;
@@ -98,7 +98,7 @@ namespace BEEV
 	  CountersAndStats("SAT Solver", bm);
     bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
-    int input_clauselist_size = cll.size();
+    // int input_clauselist_size = cll.size();
     if (cll.size() == 0)
       {
         FatalError("toSATandSolve: Nothing to Solve", ASTUndefined);    
@@ -115,7 +115,7 @@ namespace BEEV
 
     //iterate through the list (conjunction) of ASTclauses cll
     ClauseContainer::const_iterator i = cc.begin(), iend = cc.end();
-    for (int count=0, flag=0; i != iend; i++)
+    for ( ; i != iend; i++)
       {
         satSolverClause.clear();
         vector<const ASTNode*>::const_iterator j    = (*i)->begin(); 
@@ -312,7 +312,7 @@ namespace BEEV
     ClauseBuckets::iterator itend = cb->end();
 
     bool sat = false;
-    for(int count=1;it!=itend;it++, count++)
+    for(size_t count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
 	    sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm);
--- ./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()
 
+#ifdef CRYPTOMINISAT__2
   static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl)
   {
     ClausePtr c = (*(*cl).asList())[0];
     const ASTNode * a = (*c)[0];
     return *a;
   }
+#endif
 
   //########################################
   //########################################
--- ./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;
@@ -334,7 +334,7 @@ namespace BEEV
 
       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);
 
@@ -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();
+          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]);
             }
 
@@ -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;
@@ -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);
 
@@ -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 we have details of the partial products which can be true,
       int ignore = -1;
@@ -1244,7 +1244,7 @@ namespace BEEV
         ms = NULL;
 
       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), (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_back(priorSorted[k]);
         }
@@ -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);
@@ -1711,6 +1711,7 @@ namespace BEEV
 
               assert(v[i]== BBFalse);
               }
+            }
           }
         }
     }
@@ -1734,7 +1735,7 @@ namespace BEEV
         y = _x;
         }
 
-      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++)
           {
           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	2012-01-10 16:05:21.224609986 -0700
@@ -142,7 +142,7 @@ public:
                 Aig_Obj_t * pNode;
                 assert (children.size() != 0);
 
-                for (int i =0; i < children.size();i++)
+                for (size_t i =0; i < children.size();i++)
                   assert(!children[i].IsNull());
 
                 switch (kind)
--- ./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())
                             {
                                 const vector<unsigned>& v = it->second;
-                                for (int i = 0; i < v.size(); i++)
+                                for (size_t i = 0; i < v.size(); i++)
                                     satSolver.setFrozen(v[i]);
                             }
 
@@ -134,7 +134,7 @@ namespace BEEV
                         if (it2 != nodeToSATVar.end())
                             {
                                 const vector<unsigned>& v = it2->second;
-                                for (int i = 0; i < v.size(); i++)
+                                for (size_t i = 0; i < v.size(); i++)
                                     satSolver.setFrozen(v[i]);
                             }
                     }
@@ -185,7 +185,7 @@ namespace BEEV
                                         vector<unsigned> v_a;
                                         assert(ar.index_symbol.GetKind() == SYMBOL);
                                         // It was ommitted from the initial problem, so assign it freshly.
-                                        for (int i = 0; i < ar.index_symbol.GetValueWidth(); i++)
+                                        for (unsigned int i = 0; i < ar.index_symbol.GetValueWidth(); i++)
                                             {
                                                 SATSolver::Var v = satSolver.newVar();
                                                 // We probably don't want the variable eliminated.
@@ -194,7 +194,7 @@ namespace BEEV
                                             }
                                         nodeToSATVar.insert(make_pair(ar.index_symbol, v_a));
 
-                                        for (int i = 0; i < v_a.size(); i++)
+                                        for (size_t i = 0; i < v_a.size(); i++)
                                             {
                                                 SATSolver::Var var = v_a[i];
                                                 index.push(SATSolver::mkLit(var, false));
@@ -210,7 +210,7 @@ namespace BEEV
                                 if (it != nodeToSATVar.end())
                                     {
                                         vector<unsigned>& v = it->second;
-                                        for (int i = 0; i < v.size(); i++)
+                                        for (size_t i = 0; i < v.size(); i++)
                                             {
                                                 SATSolver::Var var = v[i];
                                                 value.push(SATSolver::mkLit(var, false));
@@ -219,7 +219,7 @@ namespace BEEV
                                 else if (ar.symbol.isConstant())
                                     {
                                         CBV c = ar.symbol.GetBVConst();
-                                        for (int i = 0; i < ar.symbol.GetValueWidth(); i++)
+                                        for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++)
                                             if (CONSTANTBV::BitVector_bit_test(c, i))
                                                 value_constants.push((Minisat::lbool) satSolver.true_literal());
                                             else
@@ -233,7 +233,7 @@ namespace BEEV
 
                                         assert(ar.symbol.GetKind() == SYMBOL);
                                         // It was ommitted from the initial problem, so assign it freshly.
-                                        for (int i = 0; i < ar.symbol.GetValueWidth(); i++)
+                                        for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++)
                                             {
                                                 SATSolver::Var v = satSolver.newVar();
                                                 // We probably don't want the variable eliminated.
@@ -242,7 +242,7 @@ namespace BEEV
                                             }
                                         nodeToSATVar.insert(make_pair(ar.symbol, v_a));
 
-                                        for (int i = 0; i < v_a.size(); i++)
+                                        for (size_t i = 0; i < v_a.size(); i++)
                                             {
                                                 SATSolver::Var var = v_a[i];
                                                 value.push(SATSolver::mkLit(var, false));
--- ./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;
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
   ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
 
   bool t = false;
@@ -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;
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
   ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
 
   bool t = false;
@@ -549,7 +547,6 @@ void vc_getCounterExampleArray(VC vc, Ex
 }
 
 int vc_counterexample_size(VC vc) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
   ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
 
   return ce->CounterExampleSize();
@@ -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;
-  unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits;
+  unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> (64-n_bits);
   //printf("%ull", max_n_bits);
   if(v > max_n_bits) {
     printf("CInterface: vc_bvConstExprFromInt: "\
@@ -1484,16 +1481,11 @@ Expr vc_bvWriteToMemoryArray(VC vc,
     return vc_writeExpr(vc, array, byteIndex, element);
   else {
     int count = 1;
-    int hi = newBitsPerElem - 1;
-    int low = newBitsPerElem - 8;
     int low_elem = 0;
     int hi_elem = low_elem + 7;
     Expr c = vc_bvExtract(vc, element, hi_elem, low_elem);
     Expr newarray = vc_writeExpr(vc, array, byteIndex, c);
     while(--numOfBytes > 0) {
-      hi = low-1;
-      low = low-8;
-            
       low_elem = low_elem + 8;
       hi_elem = low_elem + 7;
             
@@ -1668,7 +1660,6 @@ int vc_isBool(Expr e) {
 }
 
 void vc_Destroy(VC vc) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
   // for(std::vector<BEEV::ASTNode *>::iterator it=created_exprs.begin(),
   //    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	2012-01-10 16:05:21.226609946 -0700
@@ -210,7 +210,7 @@ void printVarDeclsToStream(ASTNodeSet& s
   		{
   			string close = "";
 
-  			for (int i =0; i < c.size()-1; i++)
+  			for (size_t i =0; i < c.size()-1; i++)
   			{
   				os << "(" << functionToSMTLIBName(kind,false);
   				os << " ";
--- ./src/printer/SMTLIB1Printer.cpp.orig	2010-06-24 23:19:52.000000000 -0600
+++ ./src/printer/SMTLIB1Printer.cpp	2012-01-10 16:05:21.226609946 -0700
@@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod
   		{
   			string close = "";
 
-  			for (int i =0; i < c.size()-1; i++)
+  			for (size_t i =0; i < c.size()-1; i++)
   			{
   				os << "(" << functionToSMTLIBName(kind,true);
   				os << " ";
--- ./src/printer/SMTLIBPrinter.h.orig	2010-05-23 20:03:46.000000000 -0600
+++ ./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);
 
 	bool containsAnyArrayOps(const ASTNode& n);
-
-	static string tolower(const char * name);
 };
 #endif
--- ./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.
 
-    int setVerbosity(int v);
+    void setVerbosity(int v);
 
     virtual uint8_t modelValue(Var x) const;
 
--- ./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	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();
 
-    int setVerbosity(int v);
+    void setVerbosity(int v);
 
     int nVars();
 
--- ./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.
   {
-    s->addClause(ps);
+    return s->addClause(ps);
   }
 
   bool
@@ -47,7 +47,7 @@ namespace BEEV
    return Minisat::toInt(s->modelValue(x));
   }
 
-  int SimplifyingMinisat::setVerbosity(int v)
+  void SimplifyingMinisat::setVerbosity(int v)
   {
     s->verbosity = v;
   }
--- ./src/sat/cryptominisat2/Logger.cpp.orig	2010-06-04 12:11:26.000000000 -0600
+++ ./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);
 
-        proof = (FILE*)fclose(proof);
-        assert(proof == NULL);
+        int err = fclose(proof);
+        assert(err == 0);
+        proof = NULL;
     }
 
     if (statistics_on) {
--- ./src/sat/cryptominisat2/FailedVarSearcher.cpp.orig	2010-07-02 08:35:28.000000000 -0600
+++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp	2012-01-10 16:05:21.229609884 -0700
@@ -261,7 +261,6 @@ const bool FailedVarSearcher::search(uin
     }*/
 
 end:
-    bool removedOldLearnts = false;
     binClauseAdded = solver.binaryClauses.size() - origBinClauses;
     //Print results
     if (solver.verbosity >= 1) printResults(myTime);
@@ -272,7 +271,6 @@ end:
         double time = cpuTime();
         if ((int)origHeapSize - (int)solver.order_heap.size() >  (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) {
             completelyDetachAndReattach();
-            removedOldLearnts = true;
         } else {
             solver.clauseCleaner->removeAndCleanAll();
         }
--- ./src/sat/CryptoMinisat.cpp.orig	2010-08-20 06:07:42.000000000 -0600
+++ ./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])));
 
-    s->addClause(v);
+    return s->addClause(v);
   }
 
   bool
@@ -61,7 +61,7 @@ namespace BEEV
     return s->newVar();
   }
 
-  int CryptoMinisat::setVerbosity(int v)
+  void CryptoMinisat::setVerbosity(int v)
   {
     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	2012-01-10 16:05:21.230609864 -0700
@@ -171,11 +171,11 @@ Solver_prop::addArray(int array_id, cons
 
     if (!ok) return false;
 
-    if (i.size() > INDEX_BIT_WIDTH || ki.size() > INDEX_BIT_WIDTH)
+    if (i.size() > (int)INDEX_BIT_WIDTH || ki.size() > (int)INDEX_BIT_WIDTH)
         {
             printf("The array propagators unfortunately don't do arbitrary precision integers yet. "
                     "With the INDICES_128BITS compile time flag STP does 128-bits on 64-bit machines compiled with GCC. "
-                    "Currently STP is compiled to use %d bit indices. "
+                    "Currently STP is compiled to use %zu bit indices. "
                     "Unfortunately your problem has array indexes of size %d bits. "
                     "STP does arbitrary precision indices with the '--oldstyle-refinement' or the '-r' flags.\n",
                     INDEX_BIT_WIDTH, std::max(i.size(), ki.size()));
@@ -1167,7 +1167,6 @@ void Solver_prop::analyze(CRef confl, ve
 
                 if (debug_print)
                     printf("%d %d\n", toInt(p), toInt(var(p)));
-                Minisat::Clause  cl= ca[confl];
 
                 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	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; }
     typedef uint128_t index_type;
+# define PRIuIT PRIu128
 #else
     typedef uint64_t index_type;
+# define PRIuIT PRIu64
 #endif
 
 #define INDEX_BIT_WIDTH (sizeof(index_type) *8)
@@ -227,7 +229,7 @@ private:
                 printf("Value Size: %d\n", value.size());
                 printClause2(value);
 
-                printf("Known Index: %ld ", isIndexConstant() ? index_constant : -1);
+                printf("Known Index: %" PRIuIT " ", isIndexConstant() ? index_constant : (index_type)-1);
                 printf("Known Value: %c\n", isValueConstant() ? 't' : 'f');
                 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	2012-01-10 16:05:21.231609844 -0700
@@ -60,7 +60,7 @@ class Option
     struct OptionLt {
         bool operator()(const Option* x, const Option* y) {
             int test1 = strcmp(x->category, y->category);
-            return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+            return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
         }
     };
 
--- ./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.
   {
-    s->addClause(ps);
+    return s->addClause(ps);
   }
 
   template <class T>
@@ -58,7 +58,7 @@ namespace BEEV
   }
 
   template <class T>
-  int MinisatCore<T>::setVerbosity(int v)
+  void MinisatCore<T>::setVerbosity(int v)
   {
     s->verbosity = v;
   }
--- ./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.
   {
-    s->addClause(ps);
+    return s->addClause(ps);
   }
 
   template <class T>
@@ -66,7 +66,7 @@ namespace BEEV
   }
 
   template <class T>
-  int MinisatCore_prop<T>::setVerbosity(int v)
+  void MinisatCore_prop<T>::setVerbosity(int v)
   {
     s->verbosity = v;
   }
--- ./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();
 
-    int setVerbosity(int v);
+    void setVerbosity(int v);
 
     int nVars();
 
--- ./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();
 
-    int setVerbosity(int v);
+    void setVerbosity(int v);
 
     int nVars();
 
--- ./src/extlib-abc/kit.h.orig	2011-02-09 18:31:59.000000000 -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
 };
 
-typedef struct Kit_Edge_t_ Kit_Edge_t;
-struct Kit_Edge_t_
+typedef union Kit_Edge_t_ Kit_Edge_t;
+union Kit_Edge_t_
 {
-    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
+    } edgeBits;
+
+    unsigned int      edgeInt;
 };
 
 typedef struct Kit_Node_t_ Kit_Node_t;
@@ -203,18 +207,18 @@ static inline void         Kit_SopShrink
 static inline void         Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube )            { cSop->pCubes[cSop->nCubes++] = uCube;   }
 static inline void         Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i )    { cSop->pCubes[i] = uCube;                }
 
-static inline Kit_Edge_t   Kit_EdgeCreate( int Node, int fCompl )                         { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge;  }
-static inline unsigned     Kit_EdgeToInt( Kit_Edge_t eEdge )                              { return (eEdge.Node << 1) | eEdge.fCompl;            }
+static inline Kit_Edge_t   Kit_EdgeCreate( int Node, int fCompl )                         { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge;  }
+static inline unsigned     Kit_EdgeToInt( Kit_Edge_t eEdge )                              { return (eEdge.edgeBits.Node << 1) | eEdge.edgeBits.fCompl; }
 static inline Kit_Edge_t   Kit_IntToEdge( unsigned Edge )                                 { return Kit_EdgeCreate( Edge >> 1, Edge & 1 );       }
-static inline unsigned     Kit_EdgeToInt_( Kit_Edge_t eEdge )                             { return *(unsigned *)&eEdge;                         }
-static inline Kit_Edge_t   Kit_IntToEdge_( unsigned Edge )                                { return *(Kit_Edge_t *)&Edge;                        }
+static inline unsigned     Kit_EdgeToInt_( Kit_Edge_t eEdge )                             { return eEdge.edgeInt;                               }
+static inline Kit_Edge_t   Kit_IntToEdge_( unsigned Edge )                                { Kit_Edge_t eEdge; eEdge.edgeInt = Edge; return eEdge; }
 
 static inline int          Kit_GraphIsConst( Kit_Graph_t * pGraph )                       { return pGraph->fConst;                              }
-static inline int          Kit_GraphIsConst0( Kit_Graph_t * pGraph )                      { return pGraph->fConst && pGraph->eRoot.fCompl;      }
-static inline int          Kit_GraphIsConst1( Kit_Graph_t * pGraph )                      { return pGraph->fConst && !pGraph->eRoot.fCompl;     }
-static inline int          Kit_GraphIsComplement( Kit_Graph_t * pGraph )                  { return pGraph->eRoot.fCompl;                        }
-static inline int          Kit_GraphIsVar( Kit_Graph_t * pGraph )                         { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; }
-static inline void         Kit_GraphComplement( Kit_Graph_t * pGraph )                    { pGraph->eRoot.fCompl ^= 1;                          }
+static inline int          Kit_GraphIsConst0( Kit_Graph_t * pGraph )                      { return pGraph->fConst && pGraph->eRoot.edgeBits.fCompl; }
+static inline int          Kit_GraphIsConst1( Kit_Graph_t * pGraph )                      { return pGraph->fConst && !pGraph->eRoot.edgeBits.fCompl; }
+static inline int          Kit_GraphIsComplement( Kit_Graph_t * pGraph )                  { return pGraph->eRoot.edgeBits.fCompl;               }
+static inline int          Kit_GraphIsVar( Kit_Graph_t * pGraph )                         { return pGraph->eRoot.edgeBits.Node < (unsigned)pGraph->nLeaves; }
+static inline void         Kit_GraphComplement( Kit_Graph_t * pGraph )                    { pGraph->eRoot.edgeBits.fCompl ^= 1;                 }
 static inline void         Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot )     { pGraph->eRoot = eRoot;                              }
 static inline int          Kit_GraphLeaveNum( Kit_Graph_t * pGraph )                      { return pGraph->nLeaves;                             }
 static inline int          Kit_GraphNodeNum( Kit_Graph_t * pGraph )                       { return pGraph->nSize - pGraph->nLeaves;             }
@@ -222,14 +226,12 @@ static inline Kit_Node_t * Kit_GraphNode
 static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph )                      { return pGraph->pNodes + pGraph->nSize - 1;          }
 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 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 int          Kit_Float2Int( float Val )     { return *((int *)&Val);               }
-static inline float        Kit_Int2Float( int Num )       { return *((float *)&Num);             }
 static inline int          Kit_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
 static inline int          Kit_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5));                             }
 static inline unsigned     Kit_BitMask( int nBits )       { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits);               }
@@ -486,6 +488,18 @@ static inline void Kit_TruthIthVar( unsi
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+extern Kit_Graph_t * Kit_GraphCreateConst0( void );
+extern Kit_Graph_t * Kit_GraphCreateConst1( void );
+extern void          Kit_GraphFree( Kit_Graph_t * );
+extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * );
+extern void          Kit_TruthCofactor0( unsigned *, int, int );
+extern void          Kit_TruthCofactor1( unsigned *, int, int );
+extern int           Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int );
+extern void          Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int );
+extern void          Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int );
+extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * );
+extern int           Kit_TruthVarInSupport( unsigned *, int, int );
+
 #if 0
 
 /*=== 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	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 )
 {
-    unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
+    unsigned uCube, uDiv, uCube2 = 0, uDiv2, uQuo;
     int i, i2, k, k2, nCubesRem;
     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	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 )
     {
-        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
-        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl ); 
+        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl ); 
         pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
     }
     // 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	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) );
     pGraph->fConst = 1;
-    pGraph->eRoot.fCompl = 1;
+    pGraph->eRoot.edgeBits.fCompl = 1;
     return pGraph;
 }
 
@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i
     Kit_Graph_t * pGraph;
     assert( 0 <= iLeaf && iLeaf < nLeaves );
     pGraph = Kit_GraphCreate( nLeaves );
-    pGraph->eRoot.Node   = iLeaf;
-    pGraph->eRoot.fCompl = fCompl;
+    pGraph->eRoot.edgeBits.Node   = iLeaf;
+    pGraph->eRoot.edgeBits.fCompl = fCompl;
     return pGraph;
 }
 
@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap
     // set the inputs and other info
     pNode->eEdge0 = eEdge0;
     pNode->eEdge1 = eEdge1;
-    pNode->fCompl0 = eEdge0.fCompl;
-    pNode->fCompl1 = eEdge1.fCompl;
+    pNode->fCompl0 = eEdge0.edgeBits.fCompl;
+    pNode->fCompl1 = eEdge1.edgeBits.fCompl;
     return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
 }
 
@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph
     // set the inputs and other info
     pNode->eEdge0 = eEdge0;
     pNode->eEdge1 = eEdge1;
-    pNode->fCompl0 = eEdge0.fCompl;
-    pNode->fCompl1 = eEdge1.fCompl;
+    pNode->fCompl0 = eEdge0.edgeBits.fCompl;
+    pNode->fCompl1 = eEdge1.edgeBits.fCompl;
     // make adjustments for the OR gate
     pNode->fNodeOr = 1;
-    pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
-    pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
+    pNode->eEdge0.edgeBits.fCompl = !pNode->eEdge0.edgeBits.fCompl;
+    pNode->eEdge1.edgeBits.fCompl = !pNode->eEdge1.edgeBits.fCompl;
     return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
 }
 
@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap
     if ( Type == 0 )
     {
         // derive the first AND
-        eEdge0.fCompl ^= 1;
+        eEdge0.edgeBits.fCompl ^= 1;
         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
-        eEdge0.fCompl ^= 1;
+        eEdge0.edgeBits.fCompl ^= 1;
         // derive the second AND
-        eEdge1.fCompl ^= 1;
+        eEdge1.edgeBits.fCompl ^= 1;
         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
         // derive the final OR
         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
@@ -238,12 +238,12 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap
         // derive the first AND
         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
         // derive the second AND
-        eEdge0.fCompl ^= 1;
-        eEdge1.fCompl ^= 1;
+        eEdge0.edgeBits.fCompl ^= 1;
+        eEdge1.edgeBits.fCompl ^= 1;
         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
         // derive the final OR
         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
-        eNode.fCompl ^= 1;
+        eNode.edgeBits.fCompl ^= 1;
     }
     return eNode;
 }
@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap
         // derive the first AND
         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
         // derive the second AND
-        eEdgeC.fCompl ^= 1;
+        eEdgeC.edgeBits.fCompl ^= 1;
         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
         // derive the final OR
         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap
     else
     {
         // complement the arguments
-        eEdgeT.fCompl ^= 1;
-        eEdgeE.fCompl ^= 1;
+        eEdgeT.edgeBits.fCompl ^= 1;
+        eEdgeE.edgeBits.fCompl ^= 1;
         // derive the first AND
         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
         // derive the second AND
-        eEdgeC.fCompl ^= 1;
+        eEdgeC.edgeBits.fCompl ^= 1;
         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
         // derive the final OR
         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
-        eNode.fCompl ^= 1;
+        eNode.edgeBits.fCompl ^= 1;
     }
     return eNode;
 }
@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t *
     // compute the function for each internal node
     Kit_GraphForEachNode( pGraph, pNode, i )
     {
-        uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
-        uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
-        uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
-        uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
+        uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc;
+        uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc;
+        uTruth0 = pNode->eEdge0.edgeBits.fCompl? ~uTruth0 : uTruth0;
+        uTruth1 = pNode->eEdge1.edgeBits.fCompl? ~uTruth1 : uTruth1;
         uTruth = uTruth0 & uTruth1;
         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	2012-01-10 16:05:21.234609784 -0700
@@ -74,8 +74,8 @@ void Aig_TableResize( Aig_Man_t * p )
 {
     Aig_Obj_t * pEntry, * pNext;
     Aig_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, i, clk;
-clk = clock();
+    int nTableSizeOld, Counter, i;
+
     // save the old table
     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	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 )
 {
     extern void Abc_ShowFile( char * FileNameDot );
-    static Counter = 0;
+    static int Counter = 0;
     char FileNameDot[200];
     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	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) )
 //        pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) );
-    else 
+    else  {
         assert( 0 );
+        pResult = NULL;
+    }
     // replace the node with buffer by the node without buffer
     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	2012-01-10 16:05:21.235609764 -0700
@@ -352,7 +352,6 @@ Cnf_Dat_t * Cnf_DeriveSimple_Additional(
     int Number = old->nVars+1;
 
     // assign variables to the PIs
-    int newPI = 0;
     Aig_ManForEachPi( p, pObj, i )
     	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	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
     };
-    unsigned uTruthRes, uCof0, uCof1;
-    int nMints, Shift, v;
+    unsigned uCof0, uCof1;
+    int Shift, v;
     assert( nVars < 6 );
-    nMints = (1 << nVars);
-    uTruthRes = uTruth;
     for ( v = 0; v < nVars; v++ )
         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	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;
     Aig_Obj_t * pAnd, * pAnd0, * pAnd1;
-    int i, Counter, LevelNew, LevelOld;
+    int i, Counter, LevelNew;
     // check for constant function or a literal
     if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) )
         return 0;
@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
     Kit_GraphForEachNode( pGraph, pNode, i )
     {
         // get the children of this node
-        pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
-        pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
+        pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.edgeBits.Node );
+        pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.edgeBits.Node );
         // get the AIG nodes corresponding to the children 
         pAnd0 = pNode0->pFunc; 
         pAnd1 = pNode1->pFunc; 
         if ( pAnd0 && pAnd1 )
         {
             // if they are both present, find the resulting node
-            pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
-            pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
+            pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.edgeBits.fCompl );
+            pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.edgeBits.fCompl );
             pAnd  = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
             // return -1 if the node is the same as the original root
             if ( Aig_Regular(pAnd) == pRoot )
@@ -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;
+//            LevelOld = (int)Aig_Regular(pAnd)->Level;
 //            assert( LevelNew == LevelOld );
         }
         if ( LevelNew > LevelMax )
@@ -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 )
     {
-        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
-        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl ); 
+        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl ); 
         pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
 /*
 printf( "Checking " );
--- ./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());
 
-    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-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++)
 		  {
-				const ASTNode& ArrName = iset->first;
 				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	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
@@ -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 == 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 == 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 (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;
 
-      for (int i = 0; i < children.size(); i++)
+      for (size_t i = 0; i < children.size(); i++)
         {
           if (children[i].GetKind() == BEEV::BVCONST)
             {
@@ -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)
@@ -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(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>();
-
-
+    else
+      newS = NULL;
 
     SATSolver& NewSolver = *newS;
 
--- ./src/parser/ParserInterface.h.orig	2011-07-09 00:56:51.000000000 -0600
+++ ./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);
           ASTVec & current = symbols.back();
-          for (int i=0; i < current.size() ;i++)
+          for (size_t i=0; i < current.size() ;i++)
               letMgr._parser_symbol_table.erase(current[i]);
           symbols.erase(symbols.end()-1);
         }
@@ -234,7 +234,7 @@ public:
 
      void printStatus()
      {
-      for (int i=0; i < cache.size();i++)
+      for (size_t i=0; i < cache.size();i++)
         {
           cache[i].print();
         }
@@ -271,7 +271,7 @@ public:
 
       // Loop through the set of assertions converting them to single nodes..
       ASTVec v;
-      for (int i = 0; i < assertionsSMT2.size(); i++)
+      for (size_t i = 0; i < assertionsSMT2.size(); i++)
         {
           if (assertionsSMT2[i].size() == 1)
             {}
@@ -310,7 +310,7 @@ public:
       // It's satisfiable, so everything beneath it is satisfiable too.
       if (last_result ==SOLVER_SATISFIABLE)
         {
-          for (int i=0; i < cache.size(); i++)
+          for (size_t i=0; i < cache.size(); i++)
               {
               assert(cache[i].result != SOLVER_UNSATISFIABLE);
               cache[i].result = SOLVER_SATISFIABLE;