summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2017-08-21 18:33:29 -0700
committerGitHub <noreply@github.com>2017-08-21 18:33:29 -0700
commit1b274e50f85762d0d894227f8fb8c72c29bf20f8 (patch)
treebbed2b12f1efa00c7781240c23230e894de6330d /src/theory
parent0ad2afe61b58725fc74423a5d90976ea9aaa6f73 (diff)
Cleanup: use Assert rather than C assert. (#1052)
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bv/aig_bitblaster.cpp2
-rw-r--r--src/theory/strings/theory_strings.cpp4
2 files changed, 3 insertions, 3 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback