summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r--src/theory/uf/theory_uf.cpp5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 111f06fe9..ef0142352 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -250,7 +250,7 @@ void TheoryUF::merge(){
(ecX->getRep()).printAst(Debug("uf"));
Debug("uf") << "right equivalence class :";
(ecY->getRep()).printAst(Debug("uf"));
-
+ Debug("uf") << std::endl;
ccUnion(ecX, ecY);
}
@@ -282,6 +282,7 @@ void TheoryUF::check(Effort level){
while(!done()){
Node assertion = get();
+ Debug("uf") << "TheoryUF::check(): " << assertion << std::endl;
switch(assertion.getKind()){
case EQUAL:
@@ -295,6 +296,8 @@ void TheoryUF::check(Effort level){
default:
Unreachable();
}
+
+ Debug("uf") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl;
}
//Make sure all outstanding merges are completed.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback