From b3f0db7abcb7195fbf2afe191e6ab4012b4971a3 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 2 Jul 2010 00:27:49 +0000
Subject: [PATCH] roll back a small change that made arith fail some asserts

---
 src/theory/theory_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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,
-- 
2.30.2