diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 6 | ||||
| -rw-r--r-- | src/theory/shared_term_manager.cpp | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7b5319267..104992bd4 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -387,11 +387,11 @@ void TheoryDatatypes::addTester( Node assertion ){ unsigned int testerIndex = -1; for( unsigned int i=0; i<possibleCons.size(); i++ ) { if( possibleCons[i] ){ - Assert( testerIndex==-1 ); + Assert( testerIndex==unsigned(-1) ); testerIndex = i; } } - Assert( testerIndex!=-1 ); + Assert( testerIndex!=unsigned(-1) ); assertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[testerIndex].getTester() ), tRep ); Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; d_em.addNode( assertionRep, exp, Reason::idt_texhaust ); @@ -862,7 +862,7 @@ void TheoryDatatypes::collectTerms( Node n ) { if( n.getKind() == APPLY_CONSTRUCTOR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ) { Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl; - bool result = d_cycle_check.addEdgeNode( n, n[i] ); + bool result CVC4_UNUSED = d_cycle_check.addEdgeNode( n, n[i] ); Assert( !result ); //this should not create any new cycles (relevant terms should have been recorded before) } }else{ diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp index 8103a149a..03afa984e 100644 --- a/src/theory/shared_term_manager.cpp +++ b/src/theory/shared_term_manager.cpp @@ -67,7 +67,7 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { uint64_t bothTags = parentTag | childTag; // Create or update the SharedData for n - SharedData* pData; + SharedData* pData = NULL; if(n.getAttribute(SharedAttr(), pData)) { // The attribute already exists, just update it if necessary uint64_t tags = pData->getTheories(); @@ -121,8 +121,8 @@ void SharedTermManager::addEq(TNode eq, Theory* thReason) { TNode x = eq[0]; TNode y = eq[1]; - SharedData* pDataX; - SharedData* pDataY; + SharedData* pDataX = NULL; + SharedData* pDataY = NULL; // Grab the SharedData for each side of the equality, create if necessary if(!x.getAttribute(SharedAttr(), pDataX)) { |