Cleanup: use Assert rather than C assert. (#1052)

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index aa67069f53a63438bd33b304e4777f496d3f4a84..5459340f6825e019fc58cc6368dad2a36fab206e 100644 (file)
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -370,7 +370,7 @@ void AigBitblaster::convertToCnfAndAssert() {
   
   Aig_Man_t * pMan = NULL;
   Cnf_Dat_t * pCnf = NULL;
-  assert( Abc_NtkIsStrash(currentAigNtk()) );
+  Assert( Abc_NtkIsStrash(currentAigNtk()) );
   
   // convert to the AIG manager
   pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 24358182f4b2e4f54876fe6cfcba44f75fbd65d7..babf77a74fd712ed85fdc97a34939c16bd5b3840 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3508,8 +3508,8 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
       Debug("strings-explain") << "Ask for explanation of " << a[i] << std::endl;
       //assert
       if(a[i].getKind() == kind::EQUAL) {
-        //assert( hasTerm(a[i][0]) );
-        //assert( hasTerm(a[i][1]) );
+        //Assert( hasTerm(a[i][0]) );
+        //Assert( hasTerm(a[i][1]) );
         Assert( areEqual(a[i][0], a[i][1]) );
         if( a[i][0]==a[i][1] ){
           exp = false;

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index f20a554e17aa10d67690665b33fdf38d9b53ad9c..016bd21840402578fce6c89c9074c1bf175b5e8f 100644 (file)
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -42,7 +42,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
   CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
   a.tv_sec += b.tv_sec;
   long nsec = a.tv_nsec + b.tv_nsec;
-  assert(nsec >= 0);
+  Assert(nsec >= 0);
   if(nsec < 0) {
     nsec += nsec_per_sec;
     --a.tv_sec;
@@ -51,7 +51,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
     nsec -= nsec_per_sec;
     ++a.tv_sec;
   }
-  assert(nsec >= 0 && nsec < nsec_per_sec);
+  Assert(nsec >= 0 && nsec < nsec_per_sec);
   a.tv_nsec = nsec;
   return a;
 }
@@ -73,7 +73,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) {
     nsec -= nsec_per_sec;
     ++a.tv_sec;
   }
-  assert(nsec >= 0 && nsec < nsec_per_sec);
+  Assert(nsec >= 0 && nsec < nsec_per_sec);
   a.tv_nsec = nsec;
   return a;
 }

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 30f330cd795db0dda67a621a9598ad66f3787e51..6e74357c6adad183b7042e91a44ecdcc4b671117 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -38,7 +38,6 @@
 
 #include <stdint.h>
 
-#include <cassert>
 #include <ctime>
 #include <iomanip>
 #include <map>