diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:27:49 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:27:49 +0000 |
| commit | b3f0db7abcb7195fbf2afe191e6ab4012b4971a3 (patch) | |
| tree | 7c45f6920e3dfc4ee474157a015229e90e5e26b7 /src | |
| parent | 83a143b1dd78e5d7f07666fbec1362dd60348116 (diff) | |
roll back a small change that made arith fail some asserts
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/theory_engine.cpp | 2 |
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, |