summaryrefslogtreecommitdiff
path: root/src/theory/uf/cardinality_extension.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/cardinality_extension.cpp')
-rw-r--r--src/theory/uf/cardinality_extension.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 25f87de2c..166df3c80 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1023,7 +1023,7 @@ int SortModel::addSplit(Region* r)
}
if (ss == b_t)
{
- CVC4Message() << "Bad split " << s << std::endl;
+ CVC5Message() << "Bad split " << s << std::endl;
AlwaysAssert(false);
}
}
@@ -1420,7 +1420,7 @@ 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;
- // CVC4Message() << "Error: constraint asserted before cardinality
+ // CVC5Message() << "Error: constraint asserted before cardinality
// for " << it->first << std::endl; Unimplemented();
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback