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.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 9a4fc8dc2..50713e2b4 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -55,7 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
TypeNode nodeType = node.getType();
if(!nodeType.isBoolean()) {
// Make the skolem to represent the ITE
- Node skolem = nodeManager->mkVar(nodeType);
+ Node skolem = nodeManager->mkSkolem(nodeType);
Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback