Stronger support for zero-performance-penalty output, and fixes and

simplifications for the "muzzled" (i.e. competition) design, which had
been broken.  Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like

  Warning() << expensiveFunction();

Also, fix some compiler warnings.

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)) {