Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

1 files changed, 9 insertions, 12 deletions

diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 0183dd6e7..dbdeccfe5 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -55,7 +55,7 @@ prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned l
 
   for (unsigned i = 0; i < assumptions.size(); ++i) {
     TNode a = assumptions[i];
-    Assert (a.getType().isBoolean());
+    Assert(a.getType().isBoolean());
     d_bitblaster->bbAtom(a);
     bool ok = d_bitblaster->assertToSat(a, false);
     if (!ok) {
@@ -91,7 +91,7 @@ prop::SatValue BVQuickCheck::checkSat(unsigned long budget) {
 }
 
 bool BVQuickCheck::addAssertion(TNode assertion) {
-  Assert (assertion.getType().isBoolean());
+  Assert(assertion.getType().isBoolean());
   d_bitblaster->bbAtom(assertion);
   // assert to sat solver and run bcp to detect easy conflicts
   bool ok = d_bitblaster->assertToSat(assertion, true);
@@ -162,9 +162,7 @@ QuickXPlain::~QuickXPlain() {}
 
 unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
                                       std::vector<TNode>& conflict) {
-
-  Assert(!d_solver->getConflict().isNull() &&
-         d_solver->inConflict());
+  Assert(!d_solver->getConflict().isNull() && d_solver->inConflict());
   Node query_confl = d_solver->getConflict();
 
   // conflict wasn't actually minimized
@@ -190,24 +188,23 @@ unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
   if (write == low) {
     return low;
   }
-  Assert (write != 0);
+  Assert(write != 0);
   unsigned new_high = write - 1;
 
   for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) {
     conflict[write++] = *it;
   }
-  Assert (write -1 == high);
-  Assert (new_high <= high);
-  
+  Assert(write - 1 == high);
+  Assert(new_high <= high);
+
   return new_high;
 }
 
 void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high,
                                            std::vector<TNode>& conflict,
                                            std::vector<TNode>& new_conflict) {
+  Assert(low <= high && high < conflict.size());
 
-  Assert (low <= high && high < conflict.size());
-  
   if (low == high) {
     new_conflict.push_back(conflict[low]);
     return;
@@ -323,7 +320,7 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
   ++d_numCalled;
   ++(d_statistics.d_numConflictsMinimized);
   TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime);
-  Assert (confl.getNumChildren() > 2);
+  Assert(confl.getNumChildren() > 2);
   std::vector<TNode> conflict;
   for (unsigned i = 0; i < confl.getNumChildren(); ++i) {
     conflict.push_back(confl[i]);