From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 22 Aug 2017 01:33:29 +0000 (-0700)
Subject: Cleanup: use Assert rather than C assert. (#1052)
X-Git-Tag: cvc5-1.0.0~5671
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1b274e50f85762d0d894227f8fb8c72c29bf20f8;p=cvc5.git

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 aa67069f5..5459340f6 100644
--- 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 24358182f..babf77a74 100644
--- 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 f20a554e1..016bd2184 100644
--- 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 30f330cd7..6e74357c6 100644
--- 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>