summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f496f1fd5..86e808d66 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -147,7 +147,7 @@ Node TheoryEngine::removeITEs(TNode node) {
TypeNode nodeType = node[1].getType();
if(!nodeType.isBoolean()){
- Node skolem = nodeManager->mkSkolem(node.getType());
+ Node skolem = nodeManager->mkVar(node.getType());
Node newAssertion =
nodeManager->mkNode(
kind::ITE,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback