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

1 files changed, 7 insertions, 6 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index f6f1de69c..b133b878e 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -517,8 +517,9 @@ public:
    * (which was previously propagated by this theory).
    */
   virtual Node explain(TNode n) {
-    Unimplemented("Theory %s propagated a node but doesn't implement the "
-                  "Theory::explain() interface!", identify().c_str());
+    Unimplemented() << "Theory " << identify()
+                    << " propagated a node but doesn't implement the "
+                       "Theory::explain() interface!";
   }
 
   /**
@@ -615,8 +616,8 @@ public:
     *  via the syntax (! n :attr)
     */
   virtual void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
-    Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface",
-                  identify().c_str());
+    Unimplemented() << "Theory " << identify()
+                    << " doesn't support Theory::setUserAttribute interface";
   }
 
   /** A set of theories */
@@ -645,7 +646,7 @@ public:
 
   /** Returns the index size of a set of theories */
   static inline size_t setIndex(TheoryId id, Set set) {
-    Assert (setContains(id, set));
+    Assert(setContains(id, set));
     size_t count = 0;
     while (setPop(set) != id) {
       ++ count;
@@ -858,7 +859,7 @@ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
 
 
 inline theory::Assertion Theory::get() {
-  Assert( !done(), "Theory::get() called with assertion queue empty!" );
+  Assert(!done()) << "Theory::get() called with assertion queue empty!";
 
   // Get the assertion
   Assertion fact = d_facts[d_factsHead];