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

1 files changed, 19 insertions, 8 deletions

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 07facf4af..9e8078a72 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -95,9 +95,9 @@ class InequalityGraph : public context::ContextNotifyObj{
       : d_model(model)
     {}
     bool operator() (TermId left, TermId right) const {
-      Assert (d_model->find(left) != d_model->end() &&
-              d_model->find(right) != d_model->end());
-      
+      Assert(d_model->find(left) != d_model->end()
+             && d_model->find(right) != d_model->end());
+
       return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; 
     }
   }; 
@@ -148,11 +148,22 @@ class InequalityGraph : public context::ContextNotifyObj{
   
   ReasonId registerReason(TNode reason);
   TNode getReasonNode(ReasonId id) const;
-  
-  
-  Edges& getEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; }
-  InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
-  const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; }
+
+  Edges& getEdges(TermId id)
+  {
+    Assert(id < d_ineqEdges.size());
+    return d_ineqEdges[id];
+  }
+  InequalityNode& getInequalityNode(TermId id)
+  {
+    Assert(id < d_ineqNodes.size());
+    return d_ineqNodes[id];
+  }
+  const InequalityNode& getInequalityNode(TermId id) const
+  {
+    Assert(id < d_ineqNodes.size());
+    return d_ineqNodes[id];
+  }
   unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
   bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }