summaryrefslogtreecommitdiff
path: root/src/util/ite_removal.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/ite_removal.cpp')
-rw-r--r--src/util/ite_removal.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 1ceedc688..1b29f9ef8 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -91,7 +91,6 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
if(node.getKind() == kind::ITE) {
TypeNode nodeType = node.getType();
if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
-Debug("ite") << "CAN REMOVE ITE " << node << " BECAUSE " << inQuant << " " << node.hasBoundVar() << endl;
Node skolem;
// Make the skolem to represent the ITE
skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback