diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-12-02 14:24:52 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-02 14:24:52 -0800 |
commit | a9eaeb438882abd6d06be41c6fcb87f4f04bcc8c (patch) | |
tree | af6188637ea86feb9f6bc6595740a2d5129893fb /src/theory/uf | |
parent | 768157d3bf78337a603004a2a47026ecf1b70612 (diff) |
Rename macro Message to CVC4Message. (#5576)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index b51e40a6c..ddf81c2e8 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1014,8 +1014,9 @@ int SortModel::addSplit(Region* r) }else{ Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl; } - if( ss==b_t ){ - Message() << "Bad split " << s << std::endl; + if (ss == b_t) + { + CVC4Message() << "Bad split " << s << std::endl; AlwaysAssert(false); } } @@ -1420,8 +1421,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ if( !it->second->hasCardinalityAsserted() ){ Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl; - //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl; - //Unimplemented(); + // CVC4Message() << "Error: constraint asserted before cardinality + // for " << it->first << std::endl; Unimplemented(); } } } |