[stp] Update to recent subversion snapshot. Minor spec file cleanups.
Jerry James
jjames at fedoraproject.org
Tue Dec 13 20:27:15 UTC 2011
commit 98f8a24ce89dbbf0c194bb9d9358d55bd1d6aeef
Author: Jerry James <loganjerry at gmail.com>
Date: Tue Dec 13 13:26:56 2011 -0700
Update to recent subversion snapshot.
Minor spec file cleanups.
.gitignore | 2 +-
sources | 2 +-
stp-strcmp.patch | 11 -
stp-warning.patch | 1977 +++++++++++++++++++++++++++++++++++++++++++++++++++++
stp.spec | 103 ++--
5 files changed, 2031 insertions(+), 64 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 57ee1ec..a214bd6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-stp-ver-0.1-11-18-2008.tgz
+/stp-0.1.tar.xz
diff --git a/sources b/sources
index def1769..ae8501f 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-940fd698173a5a09ad0d15abdda083dd stp-ver-0.1-11-18-2008.tgz
+78da1267ffbbbd8a87a02bac476f6642 stp-0.1.tar.xz
diff --git a/stp-warning.patch b/stp-warning.patch
new file mode 100644
index 0000000..5884d43
--- /dev/null
+++ b/stp-warning.patch
@@ -0,0 +1,1977 @@
+--- ./src/simplifier/UseITEContext.h.orig 2011-04-07 07:38:52.000000000 -0600
++++ ./src/simplifier/UseITEContext.h 2011-12-13 13:08:15.892474675 -0700
+@@ -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 2011-12-13 13:08:15.892474675 -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 2011-12-13 13:08:15.893474673 -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 2011-12-13 13:09:21.387399946 -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 2011-12-13 13:08:15.894474671 -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;
+ }
+ }
+ }
+@@ -914,7 +906,6 @@ Result bvLeftShiftBothWays(vector<FixedB
+ {
+ op.setFixed(i - shiftIndex, true);
+ op.setValue(i - shiftIndex, output.getValue(i));
+- result = CHANGED;
+ }
+ }
+ }
+--- ./src/simplifier/constantBitP/ConstantBitPropagation.cpp.orig 2011-09-11 06:53:41.000000000 -0600
++++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp 2011-12-13 13:08:15.896474668 -0700
+@@ -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 2011-12-13 13:08:15.897474668 -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/ConstantBitP_Arithmetic.cpp.orig 2010-11-27 20:45:32.000000000 -0700
++++ ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp 2011-12-13 13:08:15.897474668 -0700
+@@ -33,7 +33,6 @@ Result bvSubtractBothWays(vector<FixedBi
+ Addargs.push_back(¬B);
+ 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-02-25 20:56:39.000000000 -0700
++++ ./src/simplifier/FindPureLiterals.h 2011-12-13 13:08:15.897474668 -0700
+@@ -108,7 +108,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;
+
+@@ -119,7 +119,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 2011-12-13 13:08:15.898474667 -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-05-01 08:20:34.000000000 -0600
++++ ./src/simplifier/SubstitutionMap.cpp 2011-12-13 13:08:15.899474666 -0700
+@@ -366,7 +366,7 @@ void SubstitutionMap::buildDepends(const
+ 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 2011-11-18 04:12:27.000000000 -0700
++++ ./src/simplifier/simplifier.cpp 2011-12-13 13:08:15.900474665 -0700
+@@ -250,7 +250,7 @@ namespace BEEV
+ assert(false);
+ }
+
+- for (int i = 0; i < n.Degree(); i++)
++ for (size_t i = 0; i < n.Degree(); i++)
+ {
+ checkIfInSimplifyMap(n[i], visited);
+ }
+@@ -525,6 +525,7 @@ namespace BEEV
+ return getConstantBit(n[0], i);
+
+ assert(false);
++ return -1;
+ }
+
+ ASTNode
+@@ -1293,7 +1294,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));
+ }
+@@ -1655,9 +1656,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())
+@@ -1685,7 +1686,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());
+@@ -1716,7 +1717,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());
+@@ -1897,7 +1898,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]))
+ {
+@@ -2238,7 +2239,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));
+@@ -2638,7 +2638,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.
+@@ -2660,13 +2660,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;
+@@ -2683,7 +2683,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-06-15 21:54:40.000000000 -0600
++++ ./src/simplifier/consteval.cpp 2011-12-13 13:08:15.900474665 -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-04-12 20:00:29.000000000 -0600
++++ ./src/simplifier/SubstitutionMap.h 2011-12-13 13:08:15.901474664 -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-08-05 22:02:44.000000000 -0600
++++ ./src/simplifier/RemoveUnconstrained.cpp 2011-12-13 13:08:15.901474664 -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 2011-12-13 13:08:15.902474663 -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 2011-08-30 22:02:27.000000000 -0600
++++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2011-12-13 13:08:15.902474663 -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-02-01 22:39:54.000000000 -0700
++++ ./src/to-sat/ASTNode/ToSAT.cpp 2011-12-13 13:08:15.903474662 -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-01-23 06:08:12.000000000 -0700
++++ ./src/to-sat/ASTNode/ToCNF.cpp 2011-12-13 13:08:15.903474663 -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 2011-11-15 03:40:28.000000000 -0700
++++ ./src/to-sat/BitBlaster.cpp 2011-12-13 13:08:15.904474662 -0700
+@@ -299,7 +299,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
+ template <class BBNode, class BBNodeManagerT>
+ bool BitBlaster<BBNode,BBNodeManagerT>::isConstant(const BBNodeVec& v)
+ {
+- for (int i =0; i < v.size();i++)
++ for (size_t i =0; i < v.size();i++)
+ {
+ if (v[i] != nf->getTrue() && v[i] != nf->getFalse())
+ return false;
+@@ -322,7 +322,7 @@ ASTNode BitBlaster<BBNode,BBNodeManagerT
+
+ 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);
+
+@@ -640,14 +640,14 @@ const BBNodeVec BitBlaster<BBNode,BBNode
+ {
+ // Add all the children up using an addition network.
+ vector<BBNodeVec> results;
+- for (int i=0; i < term.Degree();i++)
++ for (size_t i=0; i < term.Degree();i++)
+ results.push_back(BBTerm(term[i], support));
+
+ const int bitWidth = term[0].GetValueWidth();
+ std::vector<stack<BBNode> > products(bitWidth);
+ for (int i=0; i < bitWidth;i++)
+ {
+- for (int j=0; j < results.size();j++)
++ for (size_t j=0; j < results.size();j++)
+ products[i].push(results[j][i]);
+ }
+
+@@ -1070,7 +1070,7 @@ void convert(const BBNodeVec& v, BBNodeM
+ const BBNode& BBTrue = nf->getTrue();
+ const BBNode& BBFalse = nf->getFalse();
+
+- for (int i =0; i < v.size(); i++)
++ for (size_t i =0; i < v.size(); i++)
+ {
+ if (v[i] == BBTrue)
+ result[i] = ONE_MT;
+@@ -1082,7 +1082,7 @@ void convert(const BBNodeVec& v, BBNodeM
+
+ // find runs of ones.
+ int lastOne=-1;
+- for (int i =0; i < v.size(); i++)
++ for (size_t i =0; i < v.size(); i++)
+ {
+ assert(result[i] != MINUS_ONE_MT);
+
+@@ -1092,7 +1092,7 @@ void convert(const BBNodeVec& v, BBNodeM
+ if (result[i] != ONE_MT && lastOne != -1 && (i-lastOne >=3))
+ {
+ result[lastOne] = MINUS_ONE_MT;
+- for (int j = lastOne+1; j<i;j++)
++ for (size_t j = lastOne+1; j<i;j++)
+ result[j] = ZERO_MT;
+ // Should this be lastOne = i?
+ lastOne = i;
+@@ -1105,7 +1105,7 @@ void convert(const BBNodeVec& v, BBNodeM
+ if (lastOne != -1 && (v.size() -lastOne >1))
+ {
+ result[lastOne] = MINUS_ONE_MT;
+- for (int j = lastOne+1; j< v.size();j++)
++ for (size_t j = lastOne+1; j< v.size();j++)
+ result[j] = ZERO_MT;
+ }
+ }
+@@ -1310,7 +1310,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+ cerr << "["<< ms.columnL[i] << ":"<< ms.columnH[i] << "]["<< ms.sumL[i] << ":" << ms.sumH[i] << "]";
+ }
+
+- if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
++ if (((int)products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
+ {
+ if (debug_bounds)
+ cerr << "S";
+@@ -1361,7 +1361,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
+ }
+
+ BBNodeVec notY;
+- for (int i =0 ; i < y.size();i++)
++ for (size_t i =0 ; i < y.size();i++)
+ {
+ notY.push_back(nf->CreateNode(NOT,y[i]));
+ }
+@@ -1414,7 +1414,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
+ t_products[i].push_back(BBFalse);
+
+ sort(t_products[i].begin(), t_products[i].end());
+- for (int j=0; j < t_products[i].size();j++)
++ for (size_t j=0; j < t_products[i].size();j++)
+ products[i].push(t_products[i][j]);
+ }
+ }
+@@ -1488,7 +1488,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+ {
+
+ // Add the carry from the prior column. i.e. each second sorted formula.
+- for (int k = 1; k < priorSorted.size(); k += 2)
++ for (size_t k = 1; k < priorSorted.size(); k += 2)
+ {
+ current.push(priorSorted[k]);
+ }
+@@ -1570,7 +1570,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+ FixedBits* b = cb->fixedMap->map->find(n)->second;
+ for (int i = 0; i < b->getWidth(); i++)
+ {
+- if (b->isFixed(i))
++ if (b->isFixed(i)) {
+ if (b->getValue(i))
+ {
+ assert(v[i]== BBTrue);
+@@ -1587,6 +1587,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
+
+ assert(v[i]== BBFalse);
+ }
++ }
+ }
+ }
+ }
+@@ -1701,7 +1702,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
+
+ // check if y is already zero.
+ bool isZero=true;
+- for (int i =0; i < rwidth;i++)
++ for (unsigned int i =0; i < rwidth;i++)
+ if (y[i] != nf->getFalse())
+ {
+ isZero = false;
+--- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig 2011-02-01 22:39:54.000000000 -0700
++++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2011-12-13 13:08:15.905474660 -0700
+@@ -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-11-27 19:55:18.000000000 -0700
++++ ./src/to-sat/AIG/ToSATAIG.cpp 2011-12-13 13:08:15.905474660 -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-11-10 06:01:41.000000000 -0700
++++ ./src/c_interface/c_interface.cpp 2011-12-13 13:08:15.906474658 -0700
+@@ -613,7 +613,6 @@ void vc_printCounterExample(VC vc) {
+
+ 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;
+@@ -626,7 +625,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;
+@@ -646,7 +644,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();
+@@ -1038,7 +1035,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: "\
+@@ -1581,16 +1578,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;
+
+@@ -1765,7 +1757,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 2011-12-13 13:08:15.906474658 -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 2011-12-13 13:08:15.906474658 -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 2011-12-13 13:08:15.907474657 -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 2011-06-22 20:17:24.000000000 -0600
++++ ./src/sat/SimplifyingMinisat.h 2011-12-13 13:08:15.907474657 -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 2011-10-22 06:12:28.000000000 -0600
++++ ./src/sat/SATSolver.h 2011-12-13 13:08:15.907474657 -0700
+@@ -58,7 +58,7 @@ namespace BEEV
+ virtual void setSeed(int i)
+ {}
+
+- virtual int setVerbosity(int v) =0;
++ virtual void setVerbosity(int v) =0;
+
+ virtual lbool true_literal() =0;
+ virtual lbool false_literal() =0;
+--- ./src/sat/MinisatCore_prop.h.orig 2011-10-22 06:12:28.000000000 -0600
++++ ./src/sat/MinisatCore_prop.h 2011-12-13 13:08:15.907474657 -0700
+@@ -43,7 +43,7 @@ namespace BEEV
+
+ virtual Var newVar();
+
+- int setVerbosity(int v);
++ void setVerbosity(int v);
+
+ int nVars();
+
+--- ./src/sat/SimplifyingMinisat.cpp.orig 2011-06-22 20:17:24.000000000 -0600
++++ ./src/sat/SimplifyingMinisat.cpp 2011-12-13 13:08:15.908474656 -0700
+@@ -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 2011-12-13 13:08:15.908474656 -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 2011-12-13 13:08:15.909474655 -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 2011-12-13 13:08:15.909474655 -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 2011-12-13 13:08:15.909474655 -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 2011-12-13 13:08:15.910474654 -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 2011-12-13 13:08:15.911474653 -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 2011-10-22 06:12:28.000000000 -0600
++++ ./src/sat/MinisatCore.cpp 2011-12-13 13:08:15.911474653 -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 2011-10-22 06:12:28.000000000 -0600
++++ ./src/sat/MinisatCore_prop.cpp 2011-12-13 13:08:15.911474653 -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 2010-08-20 06:07:42.000000000 -0600
++++ ./src/sat/CryptoMinisat.h 2011-12-13 13:08:15.912474651 -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 2010-08-20 06:07:42.000000000 -0600
++++ ./src/sat/MinisatCore.h 2011-12-13 13:08:15.912474651 -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 2011-12-13 13:08:15.912474651 -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 2011-12-13 13:08:15.913474649 -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 2011-12-13 13:08:15.913474649 -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 2011-12-13 13:08:15.914474647 -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 2011-12-13 13:08:15.914474647 -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 2011-12-13 13:08:15.914474647 -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 2011-12-13 13:08:15.915474646 -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 2011-12-13 13:08:15.915474646 -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 2011-12-13 13:08:15.915474646 -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 2011-12-13 13:08:15.916474646 -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,8 +263,6 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
+ LevelNew = (int)Aig_Regular(pAnd0)->Level;
+ else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) )
+ LevelNew = (int)Aig_Regular(pAnd1)->Level;
+- LevelOld = (int)Aig_Regular(pAnd)->Level;
+-// assert( LevelNew == LevelOld );
+ }
+ if ( LevelNew > LevelMax )
+ return -1;
+@@ -312,8 +310,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 2011-09-12 08:58:35.000000000 -0600
++++ ./src/AST/ASTmisc.cpp 2011-12-13 13:08:15.916474646 -0700
+@@ -76,7 +76,7 @@ bool containsArrayOps(const ASTNode& n,
+
+ visited.insert(n.GetNodeNum());
+
+- for (int i =0; i < n.Degree();i++)
++ for (size_t i =0; i < n.Degree();i++)
+ if (containsArrayOps(n[i],visited))
+ return true;
+
+--- ./src/AST/ArrayTransformer.cpp.orig 2011-09-12 08:58:35.000000000 -0600
++++ ./src/AST/ArrayTransformer.cpp 2011-12-13 13:08:15.916474646 -0700
+@@ -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 2011-11-30 06:57:18.000000000 -0700
++++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2011-12-13 13:08:15.917474646 -0700
+@@ -369,7 +369,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
+ const ASTNode& in2 = swap ? children[0] : children[1];
+ const Kind k1 = in1.GetKind();
+ const Kind k2 = in2.GetKind();
+- const int width = in1.GetValueWidth();
++ const unsigned int width = in1.GetValueWidth();
+
+ if (in1 == in2)
+ //terms are syntactically the same
+@@ -386,7 +386,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
+ if ((k1 == BEEV::BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BEEV::BVNEG && k2 == BEEV::BVCONST))
+ return NodeFactory::CreateNode(BEEV::EQ, in1[0], NodeFactory::CreateTerm(k1,width, in2 ));
+
+- if (k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
++ if ((k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST) || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
+ return NodeFactory::CreateNode(BEEV::EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 ));
+
+ if ((k1 == BEEV::BVNEG && in1[0] == in2) || (k2 == BEEV::BVNEG && in2[0] == in1))
+@@ -449,13 +449,13 @@ ASTNode SimplifyingNodeFactory::CreateSi
+ {
+ int match1 =-1, match2=-1;
+
+- for (int i =0; i < c1.size();i++)
+- for (int j =0; j < c2.size();j++)
++ for (size_t i =0; i < c1.size();i++)
++ for (size_t j =0; j < c2.size();j++)
+ {
+ if (c1[i] == c2[j])
+ {
+- match1 = i;
+- match2 = j;
++ match1 = (int)i;
++ match2 = (int)j;
+ }
+ }
+
+@@ -510,7 +510,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
+ bool foundZero=false, foundOne=false;
+ const unsigned original_width = in2[0].GetValueWidth();
+ const unsigned new_width = in2.GetValueWidth();
+- for (int i = original_width-1; i < new_width;i++)
++ for (unsigned i = original_width-1; i < new_width;i++)
+ if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i))
+ foundOne=true;
+ else
+@@ -1044,7 +1044,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
+ bool oneFound=false;
+ bool zeroFound=false;
+
+- for (int i = 0; i < children.size(); i++)
++ for (size_t i = 0; i < children.size(); i++)
+ {
+ if (children[i].GetKind() == BEEV::BVCONST)
+ {
+@@ -1063,7 +1063,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
+ else if (oneFound)
+ {
+ ASTVec new_children;
+- for (int i = 0; i < children.size(); i++)
++ for (size_t i = 0; i < children.size(); i++)
+ {
+ if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
+ new_children.push_back(children[i]);
+@@ -1103,13 +1103,14 @@ ASTNode SimplifyingNodeFactory::CreateTe
+ int end=-1;
+ BEEV::CBV c = c0.GetBVConst();
+ bool bad= false;
+- for (int i =0; i < width; i++)
++ for (unsigned i =0; i < width; i++)
+ {
+- if (CONSTANTBV::BitVector_bit_test(c,i))
++ if (CONSTANTBV::BitVector_bit_test(c,i)) {
+ if (start == -1)
+ start = i; // first one bit.
+ else if (end != -1)
+ bad = true;
++ }
+
+ if (!CONSTANTBV::BitVector_bit_test(c,i))
+ if (start != -1 && end==-1)
+@@ -1129,7 +1130,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
+ ASTNode z = bm.CreateZeroConst(start);
+ result = NodeFactory::CreateTerm(BEEV::BVCONCAT, end+1, result,z);
+ }
+- if (end < width-1)
++ if (end < (int)width-1)
+ {
+ ASTNode z = bm.CreateZeroConst(width-end-1);
+ result = NodeFactory::CreateTerm(BEEV::BVCONCAT, width, z,result);
+@@ -1190,7 +1191,6 @@ ASTNode SimplifyingNodeFactory::CreateTe
+ const unsigned outerHigh = children[1].GetUnsignedConst();
+
+ const unsigned innerLow = children[0][2].GetUnsignedConst();
+- const unsigned innerHigh = children[0][1].GetUnsignedConst();
+ result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh
+ + innerLow), bm.CreateBVConst(32, outerLow + innerLow));
+ }
+--- ./src/STPManager/STP.cpp.orig 2011-11-27 22:33:34.000000000 -0700
++++ ./src/STPManager/STP.cpp 2011-12-13 13:08:15.917474646 -0700
+@@ -61,8 +61,8 @@ namespace BEEV {
+ 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 2011-12-13 13:08:15.918474645 -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;
diff --git a/stp.spec b/stp.spec
index 666c4c3..4255001 100644
--- a/stp.spec
+++ b/stp.spec
@@ -1,48 +1,52 @@
-%global timestamp 11-18-2008
+# Upstream occasionally releases a subversion snapshot, but no "regular"
+# releases since the 0.1 release.
+%global svnver 1434
+%global svntim 20111130svn
Name: stp
Version: 0.1
-Release: 6%{?dist}
+Release: 7.%{svntim}%{?dist}
Summary: Constraint solver/decision procedure
Group: Applications/Engineering
License: MIT
URL: http://sourceforge.net/projects/stp-fast-prover/
-Source0: http://downloads.sourceforge.net/stp-fast-prover/stp-ver-%{version}-%{timestamp}.tgz
-
-# Minor patch to fix a missing #include for strcmp (modern g++ requires it)
-Patch1: stp-strcmp.patch
-
-# Note: This version does not support the SMT-LIB input format (the code
-# is not complete). The SourceForge SVN contains patches that
-# add SMT-LIB support.
-
-BuildRoot: %(mktemp -ud %{_tmppath}/%{name}-%{version}-%{release}-XXXXXX)
-
-BuildRequires: bison
-BuildRequires: flex
-# Requires:
+# The source for this package was pulled from upstream's subversion repository.
+# Use the following commands to generate the tarball:
+#
+# svn export -r %%{svnver} \
+# https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp \
+# stp-0.1
+# tar cvJf stp-0.1.tar.xz stp-0.1
+Source0: stp-%{version}.tar.xz
+# This patch has not yet been sent upstream. Fix a bunch of compiler warnings
+# that may indicate miscompiled code.
+Patch0: stp-warning.patch
+
+BuildRequires: bison
+BuildRequires: boost-devel
+BuildRequires: flex
+BuildRequires: valgrind
+BuildRequires: zlib-devel
%description
-STP (Simple Theorem Prover) is
-a constraint solver (also referred to as a decision procedure
-or automated prover) aimed at solving constraints generated by program
-analysis tools, theorem provers, automated bug finders, intelligent
-fuzzers and model checkers. STP has been used in many research projects
-at Stanford, Berkeley, MIT, CMU and other universities, as well as
-companies and government agencies.
+STP (Simple Theorem Prover) is a constraint solver (also referred to as
+a decision procedure or automated prover) aimed at solving constraints
+generated by program analysis tools, theorem provers, automated bug
+finders, intelligent fuzzers and model checkers. STP has been used in
+many research projects at Stanford, Berkeley, MIT, CMU and other
+universities, as well as companies and government agencies.
The input to STP are formulas over the theory of bit-vectors and arrays
-(This theory captures most expressions from languages like C/C++/Java
+(this theory captures most expressions from languages like C/C++/Java
and Verilog), and the output of STP is a single bit of information that
-indicates whether the formula is satisfiable or not. If the input is
-satisfiable, then it also generates a variable assignment to satisfy
-the input formula.
+indicates whether the formula is satisfiable or not. If the input is
+satisfiable, then it also generates a variable assignment to satisfy the
+input formula.
Additional information can be found at:
http://people.csail.mit.edu/vganesh/STP_files/stp.html
-
%package devel
Summary: Development files for STP constraint solver/decision procedure
Group: Applications/Engineering
@@ -63,54 +67,52 @@ Provides: %{name}-static = %{version}-%{release}
%description devel
Development files for the STP (Simple Theorem Prover),
a constraint solver (also referred to as a decision procedure
-or automated prover). Provides a static library.>>>>>> 1.84
+or automated prover). Provides a static library.
%prep
-%setup -q -n stp-ver-%{version}-%{timestamp}
-%patch1
+%setup -q
+%patch0
+
+# Make sure nothing uses the shipped boost sources
+rm -fr src/boost
+
+# We do not want to know about the order of member initializers
+sed -i "s/\(-Wno-deprecated\)/\1 -Wno-reorder/" scripts/Makefile.common
+
+# Avoid a BR on subversion, as well as subversion version hell
+sed -i "s|\`svnversion \$(TOP)\`|%{svnver}|" src/main/Makefile
%build
-# The true --libdir hack works around an rpmlint bug; this configure
-# doesn't accept a --libdir argument. We'll override LIB_DIR instead.
-./configure --with-prefix=%{_prefix} ; true --libdir=%{_libdir}
+scripts/configure --with-prefix=%{_prefix}
# DO NOT use _smp_mflags; build will fail.
-make -k CPPFLAGS="%{optflags} -Wno-deprecated" LIB_DIR=%{_libdir} all
+make %{?_smp_mflags} all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir}
%check
make regressall
%install
-rm -rf %{buildroot}
mkdir -p %{buildroot}%{_bindir}
mkdir -p %{buildroot}%{_includedir}/stp
mkdir -p %{buildroot}%{_libdir}
-# This "make install" doesn't support DESTDIR=%{buildroot}.
+# This "make install" doesn't support DESTDIR=%%{buildroot}.
# We'll rig PREFIX/LIB_DIR, since that happens to work for this makefile.
make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir}
-%clean
-rm -rf %{buildroot}
-
-
-# Note: Limit the files included in _libdir, or we'll accidentally
-# include the optional debugging files into the main package:
-# In the future, perhaps create a "-devel" package with:
%files
-%defattr(-,root,root,-)
%{_bindir}/*
-%doc README LICENSE
-%doc TALKS/*
-%doc PAPERS/*
-%doc web/*
+%doc AUTHORS README LICENSE LICENSE_COMPONENTS papers
%files devel
-%defattr(-,root,root,-)
%{_libdir}/libstp*.a
%{_includedir}/stp/
%changelog
+* Tue Dec 13 2011 Jerry James <loganjerry at gmail.com> - 0.1-7.20111130svn
+- Update to recent subversion snapshot
+- Minor spec file cleanups
+
* Wed Feb 09 2011 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 0.1-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
@@ -133,4 +135,3 @@ rm -rf %{buildroot}
* Mon Feb 23 2009 David A. Wheeler <dwheeler at, dwheeler.com> 0.1-1
- Initial packaging
-
More information about the scm-commits
mailing list