diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-21 18:33:29 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-08-21 18:33:29 -0700 |
| commit | 1b274e50f85762d0d894227f8fb8c72c29bf20f8 (patch) | |
| tree | bbed2b12f1efa00c7781240c23230e894de6330d /src | |
| parent | 0ad2afe61b58725fc74423a5d90976ea9aaa6f73 (diff) | |
Cleanup: use Assert rather than C assert. (#1052)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 2 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 | ||||
| -rw-r--r-- | src/util/statistics_registry.cpp | 6 | ||||
| -rw-r--r-- | src/util/statistics_registry.h | 1 |
4 files changed, 6 insertions, 7 deletions
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> |