diff --git a/.gitignore b/.gitignore index a8345f8..5b1cb69 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1 @@ -/stp-stp-fe766c9.tar.gz +/stp-stp-f8a392d.tar.gz diff --git a/sources b/sources index 2182b29..53178ac 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -3104c3fcb6e89da91f766e9b61dd87d9 stp-stp-fe766c9.tar.gz +2ec158d56d2189d07aa09e3e05c88ca2 stp-stp-f8a392d.tar.gz diff --git a/stp-warning.patch b/stp-warning.patch index a7bfb95..cace45d 100644 --- a/stp-warning.patch +++ b/stp-warning.patch @@ -1,81 +1,5 @@ -diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp -index 0e028c4..7cfa7a7 100644 ---- a/src/AST/ASTmisc.cpp -+++ b/src/AST/ASTmisc.cpp -@@ -154,7 +154,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); - } - -diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp -index 9c18b69..4fc3320 100644 ---- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp -+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp -@@ -389,7 +389,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) - 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 -@@ -526,7 +526,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) - 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 -@@ -1176,10 +1176,12 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & - for (size_t i = 0; i < width; i++) - { - if (CONSTANTBV::BitVector_bit_test(c, i)) -- if (start == -1) -- start = i; // first one bit. -- else if (end != -1) -- bad = true; -+ { -+ 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) -@@ -1200,7 +1202,7 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & - 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); -diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp -index 395e737..ff5cc3d 100644 ---- a/src/STPManager/STP.cpp -+++ b/src/STPManager/STP.cpp -@@ -576,7 +576,7 @@ namespace BEEV { - - ToSATAIG toSATAIG(bm, cb, arrayTransformer); - -- ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; -+ ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG; - - if (bm->soft_timeout_expired) - return SOLVER_TIMEOUT; -diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp -index 4ce3767..b5c061f 100644 ---- a/src/absrefine_counterexample/AbstractionRefinement.cpp -+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp +--- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2014-04-29 14:34:45.618479266 -0600 @@ -119,7 +119,7 @@ namespace BEEV } return result; @@ -94,10 +18,8 @@ index 4ce3767..b5c061f 100644 { applyAxiomToSAT(SatSolver, toBe[i], satVar); } -diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp -index 0f52bce..4029a53 100644 ---- a/src/absrefine_counterexample/CounterExample.cpp -+++ b/src/absrefine_counterexample/CounterExample.cpp +--- ./src/absrefine_counterexample/CounterExample.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/absrefine_counterexample/CounterExample.cpp 2014-04-29 14:34:45.618479266 -0600 @@ -48,7 +48,7 @@ namespace BEEV assert(symbol.GetKind() == SYMBOL); vector bitVector_array(symbolWidth,false); @@ -116,10 +38,65 @@ index 0f52bce..4029a53 100644 { if (v[i] == ~((unsigned)0)) // nb. special value. continue; -diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp -index dd761d3..2876211 100644 ---- a/src/c_interface/c_interface.cpp -+++ b/src/c_interface/c_interface.cpp +--- ./src/AST/ASTmisc.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/AST/ASTmisc.cpp 2014-04-29 14:34:45.617479267 -0600 +@@ -154,7 +154,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/NodeFactory/SimplifyingNodeFactory.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2014-04-29 14:34:45.618479266 -0600 +@@ -389,7 +389,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 +@@ -526,7 +526,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 +@@ -1188,10 +1188,12 @@ SimplifyingNodeFactory::CreateTerm(Kind + for (size_t i = 0; i < width; i++) + { + if (CONSTANTBV::BitVector_bit_test(c, i)) +- if (start == -1) +- start = i; // first one bit. +- else if (end != -1) +- bad = true; ++ { ++ 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) +@@ -1212,7 +1214,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); +--- ./src/c_interface/c_interface.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/c_interface/c_interface.cpp 2014-04-29 14:34:45.619479265 -0600 @@ -989,7 +989,7 @@ Expr vc_bvConstExprFromInt(VC vc, bmstar b = (bmstar)(((stpstar)vc)->bm); @@ -129,10 +106,8 @@ index dd761d3..2876211 100644 //printf("%ull", max_n_bits); if(v > max_n_bits) { printf("CInterface: vc_bvConstExprFromInt: "\ -diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp -index 4da3685..3ce0c3e 100644 ---- a/src/cpp_interface/cpp_interface.cpp -+++ b/src/cpp_interface/cpp_interface.cpp +--- ./src/cpp_interface/cpp_interface.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/cpp_interface/cpp_interface.cpp 2014-04-29 14:34:45.619479265 -0600 @@ -47,7 +47,7 @@ namespace BEEV // It's satisfiable, so everything beneath it is satisfiable too. if (last_result == SOLVER_SATISFIABLE) @@ -142,11 +117,9 @@ index 4da3685..3ce0c3e 100644 { assert(cache[i].result != SOLVER_UNSATISFIABLE); cache[i].result = SOLVER_SATISFIABLE; -diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c -index ae8fa8b..a88f493 100644 ---- a/src/extlib-abc/aig/aig/aigShow.c -+++ b/src/extlib-abc/aig/aig/aigShow.c -@@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * +--- ./src/extlib-abc/aig/aig/aigShow.c.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/extlib-abc/aig/aig/aigShow.c 2014-04-29 14:34:45.619479265 -0600 +@@ -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 ); @@ -155,11 +128,9 @@ index ae8fa8b..a88f493 100644 char FileNameDot[200]; FILE * pFile; // create the file name -diff --git a/src/extlib-abc/aig/dar/darRefact.c b/src/extlib-abc/aig/dar/darRefact.c -index d744b4f..83fb3b0 100644 ---- a/src/extlib-abc/aig/dar/darRefact.c -+++ b/src/extlib-abc/aig/dar/darRefact.c -@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K +--- ./src/extlib-abc/aig/dar/darRefact.c.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/extlib-abc/aig/dar/darRefact.c 2014-04-29 14:34:45.619479265 -0600 +@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig Kit_GraphForEachNode( pGraph, pNode, i ) { // get the children of this node @@ -180,7 +151,7 @@ index d744b4f..83fb3b0 100644 pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 ); // return -1 if the node is the same as the original root if ( Aig_Regular(pAnd) == pRoot ) -@@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_ +@@ -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 ) { @@ -191,11 +162,9 @@ index d744b4f..83fb3b0 100644 pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 ); /* printf( "Checking " ); -diff --git a/src/extlib-abc/aig/kit/kitAig.c b/src/extlib-abc/aig/kit/kitAig.c -index de301f2..15d39d6 100644 ---- a/src/extlib-abc/aig/kit/kitAig.c -+++ b/src/extlib-abc/aig/kit/kitAig.c -@@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph ) +--- ./src/extlib-abc/aig/kit/kitAig.c.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/extlib-abc/aig/kit/kitAig.c 2014-04-29 14:34:45.619479265 -0600 +@@ -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 ) { @@ -206,10 +175,8 @@ index de301f2..15d39d6 100644 pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 ); } // complement the result if necessary -diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c -index 39ef587..1ae5891 100644 ---- a/src/extlib-abc/aig/kit/kitGraph.c -+++ b/src/extlib-abc/aig/kit/kitGraph.c +--- ./src/extlib-abc/aig/kit/kitGraph.c.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/extlib-abc/aig/kit/kitGraph.c 2014-04-29 14:34:45.620479263 -0600 @@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0() pGraph = ALLOC( Kit_Graph_t, 1 ); memset( pGraph, 0, sizeof(Kit_Graph_t) ); @@ -219,7 +186,7 @@ index 39ef587..1ae5891 100644 return pGraph; } -@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl ) +@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i Kit_Graph_t * pGraph; assert( 0 <= iLeaf && iLeaf < nLeaves ); pGraph = Kit_GraphCreate( nLeaves ); @@ -230,7 +197,7 @@ index 39ef587..1ae5891 100644 return pGraph; } -@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg +@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap // set the inputs and other info pNode->eEdge0 = eEdge0; pNode->eEdge1 = eEdge1; @@ -241,7 +208,7 @@ index 39ef587..1ae5891 100644 return Kit_EdgeCreate( pGraph->nSize - 1, 0 ); } -@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge +@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph // set the inputs and other info pNode->eEdge0 = eEdge0; pNode->eEdge1 = eEdge1; @@ -258,7 +225,7 @@ index 39ef587..1ae5891 100644 return Kit_EdgeCreate( pGraph->nSize - 1, 1 ); } -@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg +@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap if ( Type == 0 ) { // derive the first AND @@ -273,7 +240,7 @@ index 39ef587..1ae5891 100644 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_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg +@@ -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 @@ -289,7 +256,7 @@ index 39ef587..1ae5891 100644 } return eNode; } -@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg +@@ -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 @@ -298,7 +265,7 @@ index 39ef587..1ae5891 100644 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_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg +@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap else { // complement the arguments @@ -319,7 +286,7 @@ index 39ef587..1ae5891 100644 } return eNode; } -@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph ) +@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * // compute the function for each internal node Kit_GraphForEachNode( pGraph, pNode, i ) { @@ -334,22 +301,19 @@ index 39ef587..1ae5891 100644 uTruth = uTruth0 & uTruth1; pNode->pFunc = (void *)(long)uTruth; } -diff --git a/src/extlib-abc/kit.h b/src/extlib-abc/kit.h -index af3a1a8..963a977 100644 ---- a/src/extlib-abc/kit.h -+++ b/src/extlib-abc/kit.h +--- ./src/extlib-abc/kit.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/extlib-abc/kit.h 2014-04-29 14:34:45.620479263 -0600 @@ -53,11 +53,14 @@ struct Kit_Sop_t_ unsigned * pCubes; // the storage for cubes }; -typedef struct Kit_Edge_t_ Kit_Edge_t; -struct Kit_Edge_t_ --{ -- unsigned fCompl : 1; // the complemented bit -- unsigned Node : 30; // the decomposition node pointed by the edge +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 @@ -358,7 +322,7 @@ index af3a1a8..963a977 100644 }; typedef struct Kit_Node_t_ Kit_Node_t; -@@ -203,18 +206,18 @@ static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew ) +@@ -203,18 +206,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; } @@ -386,7 +350,7 @@ index af3a1a8..963a977 100644 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 +225,12 @@ static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i ) +@@ -222,14 +225,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; } @@ -405,7 +369,7 @@ index af3a1a8..963a977 100644 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 +487,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar ) +@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsi /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -424,10 +388,8 @@ index af3a1a8..963a977 100644 #if 0 /*=== kitBdd.c ==========================================================*/ -diff --git a/src/parser/smt2.y b/src/parser/smt2.y -index c48ddaf..f756d66 100644 ---- a/src/parser/smt2.y -+++ b/src/parser/smt2.y +--- ./src/parser/smt2.y.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/parser/smt2.y 2014-04-29 14:34:45.620479263 -0600 @@ -239,7 +239,7 @@ cmdi: {} | LPAREN_TOK PUSH_TOK NUMERAL_TOK RPAREN_TOK @@ -446,7 +408,7 @@ index c48ddaf..f756d66 100644 parserInterface->pop(); parserInterface->success(); } -@@ -307,7 +307,7 @@ STRING_TOK LPAREN_TOK function_params RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVE +@@ -307,7 +307,7 @@ STRING_TOK LPAREN_TOK function_params RP BEEV::parserInterface->storeFunction(*$1, *$3, *$11); // Next time the variable is used, we want it to be fresh. @@ -455,7 +417,7 @@ index c48ddaf..f756d66 100644 BEEV::parserInterface->removeSymbol((*$3)[i]); delete $1; -@@ -321,7 +321,7 @@ STRING_TOK LPAREN_TOK function_params RPAREN_TOK BOOL_TOK an_formula +@@ -321,7 +321,7 @@ STRING_TOK LPAREN_TOK function_params RP BEEV::parserInterface->storeFunction(*$1, *$3, *$6); // Next time the variable is used, we want it to be fresh. @@ -464,11 +426,9 @@ index c48ddaf..f756d66 100644 BEEV::parserInterface->removeSymbol((*$3)[i]); delete $1; -diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp -index 7129f50..21a5855 100644 ---- a/src/printer/SMTLIB1Printer.cpp -+++ b/src/printer/SMTLIB1Printer.cpp -@@ -215,7 +215,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os) +--- ./src/printer/SMTLIB1Printer.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/printer/SMTLIB1Printer.cpp 2014-04-29 14:34:45.621479262 -0600 +@@ -215,7 +215,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod { string close = ""; @@ -477,11 +437,9 @@ index 7129f50..21a5855 100644 { os << "(" << functionToSMTLIBName(kind,true); os << " "; -diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp -index 5ee4e98..d446897 100644 ---- a/src/printer/SMTLIB2Printer.cpp -+++ b/src/printer/SMTLIB2Printer.cpp -@@ -213,7 +213,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) +--- ./src/printer/SMTLIB2Printer.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/printer/SMTLIB2Printer.cpp 2014-04-29 14:34:45.621479262 -0600 +@@ -213,7 +213,7 @@ void printVarDeclsToStream(ASTNodeSet& s { string close = ""; @@ -490,10 +448,8 @@ index 5ee4e98..d446897 100644 { os << "(" << functionToSMTLIBName(kind,false); os << " "; -diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h -index e74df19..eaf0c9d 100644 ---- a/src/simplifier/AlwaysTrue.h -+++ b/src/simplifier/AlwaysTrue.h +--- ./src/simplifier/AlwaysTrue.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/AlwaysTrue.h 2014-04-29 14:34:45.621479262 -0600 @@ -85,7 +85,7 @@ public: else new_state = state; @@ -503,10 +459,97 @@ index e74df19..eaf0c9d 100644 { newChildren.push_back(visit(n[i],new_state,fromTo)); } -diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h -index 7c762b1..34c92c1 100644 ---- a/src/simplifier/EstablishIntervals.h -+++ b/src/simplifier/EstablishIntervals.h +--- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2014-04-29 14:34:45.623479259 -0600 +@@ -129,6 +129,7 @@ fast_exit(FixedBits& c0, FixedBits& c1) + } + return false; + } ++ return true; + } + + +--- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp 2014-04-29 14:34:45.623479259 -0600 +@@ -157,14 +157,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/ConstantBitPropagation.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp 2014-04-29 14:34:45.623479259 -0600 +@@ -433,7 +433,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]); + } + +@@ -469,7 +469,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/FixedBits.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/constantBitP/FixedBits.cpp 2014-04-29 14:34:45.623479259 -0600 +@@ -382,7 +382,7 @@ namespace simplifier + void + FixedBits::fromUnsigned(unsigned val) + { +- for (unsigned i = 0; i < width; i++) ++ for (unsigned i = 0; i < (unsigned) width; i++) + { + if (i < (unsigned) width && i < sizeof(unsigned) * 8) + { +--- ./src/simplifier/constantBitP/MersenneTwister.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/constantBitP/MersenneTwister.h 2014-04-29 14:34:45.623479259 -0600 +@@ -231,7 +231,7 @@ inline void MTRand::seed( uint32 *const + initialize(19650218UL); + int i = 1; + uint32 j = 0; +- int k = ( N > seedLength ? N : seedLength ); ++ int k = ( N > seedLength ? (int) N : seedLength ); + for( ; k; --k ) + { + state[i] = +--- ./src/simplifier/consteval.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/consteval.cpp 2014-04-29 14:34:45.624479258 -0600 +@@ -37,13 +37,13 @@ namespace BEEV + CBV tmp0 = NULL; + CBV tmp1 = NULL; + +- unsigned int number_of_children = input_children.size(); ++ size_t number_of_children = input_children.size(); + assert(number_of_children >=1); + assert(k != BVCONST); + + ASTVec children; + children.reserve(number_of_children); +- for (int i =0; i < number_of_children; i++) ++ for (size_t i =0; i < number_of_children; i++) + { + if (input_children[i].isConstant()) + children.push_back(input_children[i]); +--- ./src/simplifier/EstablishIntervals.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/EstablishIntervals.h 2014-04-29 14:34:45.621479262 -0600 @@ -120,7 +120,7 @@ namespace BEEV ASTVec new_children; new_children.reserve(result.GetChildren().size()); @@ -626,10 +669,8 @@ index 7c762b1..34c92c1 100644 CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]); likeAutoPtr.clear(); -diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h -index 4b03916..4ff05bc 100644 ---- a/src/simplifier/FindPureLiterals.h -+++ b/src/simplifier/FindPureLiterals.h +--- ./src/simplifier/FindPureLiterals.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/FindPureLiterals.h 2014-04-29 14:34:45.621479262 -0600 @@ -111,7 +111,7 @@ public: { case AND: @@ -648,10 +689,8 @@ index 4b03916..4ff05bc 100644 build(n[i],polarity); break; } -diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h -index 3e9a8e2..4d37b8e 100644 ---- a/src/simplifier/MutableASTNode.h -+++ b/src/simplifier/MutableASTNode.h +--- ./src/simplifier/MutableASTNode.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/MutableASTNode.h 2014-04-29 14:34:45.621479262 -0600 @@ -46,12 +46,12 @@ public: vector tempChildren; tempChildren.reserve(n.Degree()); @@ -712,10 +751,8 @@ index 3e9a8e2..4d37b8e 100644 delete all[i]; all.clear(); } -diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp -index 09534ee..5facb98 100644 ---- a/src/simplifier/PropagateEqualities.cpp -+++ b/src/simplifier/PropagateEqualities.cpp +--- ./src/simplifier/PropagateEqualities.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/PropagateEqualities.cpp 2014-04-29 14:34:45.622479260 -0600 @@ -31,10 +31,10 @@ namespace BEEV bool result = false; @@ -742,10 +779,8 @@ index 09534ee..5facb98 100644 if (j != i) others.push_back(lhs[j]); -diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp -index ca5dd81..0fa3803 100644 ---- a/src/simplifier/RemoveUnconstrained.cpp -+++ b/src/simplifier/RemoveUnconstrained.cpp +--- ./src/simplifier/RemoveUnconstrained.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/RemoveUnconstrained.cpp 2014-04-29 14:34:45.622479260 -0600 @@ -55,7 +55,7 @@ namespace BEEV bool allChildrenAreUnconstrained(vector children) @@ -827,177 +862,8 @@ index ca5dd81..0fa3803 100644 if (children[i] != var) other.push_back(mutable_children[i]->toASTNode(nf)); -diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp -index 5a2abd5..d7a2a61 100644 ---- a/src/simplifier/SubstitutionMap.cpp -+++ b/src/simplifier/SubstitutionMap.cpp -@@ -216,7 +216,7 @@ namespace BEEV - 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. -diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h -index 5d95d39..45f8d2f 100644 ---- a/src/simplifier/UseITEContext.h -+++ b/src/simplifier/UseITEContext.h -@@ -28,7 +28,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) -@@ -86,7 +86,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)); - } - -diff --git a/src/simplifier/VariablesInExpression.cpp b/src/simplifier/VariablesInExpression.cpp -index 0bdc37f..656a5a7 100644 ---- a/src/simplifier/VariablesInExpression.cpp -+++ b/src/simplifier/VariablesInExpression.cpp -@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbol(const ASTNode& n) { - } - - vector 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::SetofVarsSeenInTerm(Symbols* symbol, bool& d - vector 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::VarSeenInTerm(const ASTNode& var, - 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; - -diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp -index 7958269..1dded88 100644 ---- a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp -+++ b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp -@@ -129,6 +129,7 @@ fast_exit(FixedBits& c0, FixedBits& c1) - } - return false; - } -+ return true; - } - - -diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp -index dea6eb1..4d8f64c 100644 ---- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp -+++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp -@@ -157,14 +157,14 @@ Result bvUnsignedQuotientAndRemainder(vector& children, - 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); - } - -diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp -index d4f5319..8ac4a37 100644 ---- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp -+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp -@@ -433,7 +433,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]); - } - -@@ -469,7 +469,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])) -diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp -index 273175a..1fe1686 100644 ---- a/src/simplifier/constantBitP/FixedBits.cpp -+++ b/src/simplifier/constantBitP/FixedBits.cpp -@@ -382,7 +382,7 @@ namespace simplifier - void - FixedBits::fromUnsigned(unsigned val) - { -- for (unsigned i = 0; i < width; i++) -+ for (unsigned i = 0; i < (unsigned) width; i++) - { - if (i < (unsigned) width && i < sizeof(unsigned) * 8) - { -diff --git a/src/simplifier/constantBitP/MersenneTwister.h b/src/simplifier/constantBitP/MersenneTwister.h -index bd63d31..238fa3f 100644 ---- a/src/simplifier/constantBitP/MersenneTwister.h -+++ b/src/simplifier/constantBitP/MersenneTwister.h -@@ -231,7 +231,7 @@ inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength ) - initialize(19650218UL); - int i = 1; - uint32 j = 0; -- int k = ( N > seedLength ? N : seedLength ); -+ int k = ( N > seedLength ? (int) N : seedLength ); - for( ; k; --k ) - { - state[i] = -diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp -index 46ac6e8..24cdbf6 100644 ---- a/src/simplifier/consteval.cpp -+++ b/src/simplifier/consteval.cpp -@@ -37,13 +37,13 @@ namespace BEEV - CBV tmp0 = NULL; - CBV tmp1 = NULL; - -- unsigned int number_of_children = input_children.size(); -+ size_t number_of_children = input_children.size(); - assert(number_of_children >=1); - assert(k != BVCONST); - - ASTVec children; - children.reserve(number_of_children); -- for (int i =0; i < number_of_children; i++) -+ for (size_t i =0; i < number_of_children; i++) - { - if (input_children[i].isConstant()) - children.push_back(input_children[i]); -diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp -index b309a8a..76cfb04 100644 ---- a/src/simplifier/simplifier.cpp -+++ b/src/simplifier/simplifier.cpp +--- ./src/simplifier/simplifier.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/simplifier.cpp 2014-04-29 14:34:45.624479258 -0600 @@ -248,7 +248,7 @@ namespace BEEV assert(false); } @@ -1099,10 +965,79 @@ index b309a8a..76cfb04 100644 newChildren.push_back( nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i], _bm->CreateBVConst(32, output.GetValueWidth() - 1), -diff --git a/src/to-sat/ASTNode/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp -index 9fa5ebc..72d41b5 100644 ---- a/src/to-sat/ASTNode/ToSAT.cpp -+++ b/src/to-sat/ASTNode/ToSAT.cpp +--- ./src/simplifier/SubstitutionMap.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/SubstitutionMap.cpp 2014-04-29 14:34:45.622479260 -0600 +@@ -216,7 +216,7 @@ namespace BEEV + 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/UseITEContext.h.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/UseITEContext.h 2014-04-29 14:34:45.622479260 -0600 +@@ -28,7 +28,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) +@@ -86,7 +86,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/VariablesInExpression.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/simplifier/VariablesInExpression.cpp 2014-04-29 14:34:45.622479260 -0600 +@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbo + } + + vector 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 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/STPManager/STP.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/STPManager/STP.cpp 2014-04-29 14:34:45.618479266 -0600 +@@ -576,7 +576,7 @@ namespace BEEV { + + ToSATAIG toSATAIG(bm, cb, arrayTransformer); + +- ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; ++ ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG; + + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; +--- ./src/to-sat/ASTNode/ToSAT.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/to-sat/ASTNode/ToSAT.cpp 2014-04-29 14:34:45.625479256 -0600 @@ -53,7 +53,7 @@ namespace BEEV // Copies the symbol into the map that is used to build the counter example. @@ -1121,10 +1056,8 @@ index 9fa5ebc..72d41b5 100644 { ClauseList *cl = (*it).second; sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm); -diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp -index 401119c..d72ffa6 100644 ---- a/src/to-sat/BitBlaster.cpp -+++ b/src/to-sat/BitBlaster.cpp +--- ./src/to-sat/BitBlaster.cpp.orig 2014-04-02 11:47:21.000000000 -0600 ++++ ./src/to-sat/BitBlaster.cpp 2014-04-29 14:34:45.625479256 -0600 @@ -1678,13 +1678,13 @@ namespace BEEV assert(ms->x.getWidth() == ms->y.getWidth()); assert(ms->r.getWidth() == ms->y.getWidth()); diff --git a/stp.spec b/stp.spec index 904b4f0..b70b2db 100644 --- a/stp.spec +++ b/stp.spec @@ -1,13 +1,13 @@ # Upstream occasionally releases a subversion snapshot, but no "regular" # releases since the 0.1 release. -%global gitdate 20140319 -%global gittag fe766c9add6f80453ec14f4a3b4d5cf3a0385551 -%global shorttag %(echo %{gittag} | cut -b -7) +%global gitdate 20140402 +%global gittag f8a392dea3e6942897e2213e13f23cf99d323ef4 +%global shorttag %(cut -b -7 <<< %{gittag}) %global user stp Name: stp Version: 0.1 -Release: 19.%{gitdate}git.%{shorttag}%{?dist} +Release: 20.%{gitdate}git.%{shorttag}%{?dist} Summary: Constraint solver/decision procedure Group: Applications/Engineering @@ -72,6 +72,7 @@ sed -i "s/-Wno-deprecated/& -Wno-reorder/" CMakeLists.txt %build %cmake +make %{?_smp_mflags} %install make install DESTDIR=%{buildroot} @@ -93,6 +94,9 @@ fi %{_libdir}/cmake/STP/ %changelog +* Tue Apr 29 2014 Jerry James - 0.1-20.20140402git.f8a392d +- Update to recent git snapshot + * Wed Mar 19 2014 Jerry James - 0.1-19.20140319git.6110a49 - Update to recent git snapshot, now hosted on github - Build now uses cmake