diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 476091723..1a0b25ade 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -98,10 +98,9 @@ Node TheoryEngine::removeITEs(TNode node) { } if(node.getKind() == kind::ITE){ - if(theoryOf(node[1]) != &d_bool && node[1].getKind() != kind::EQUAL) { - Assert( node.getNumChildren() == 3 ); - - Debug("ite") << theoryOf(node[1]) << " " << &d_bool <<endl; + Assert( node.getNumChildren() == 3 ); + TypeNode nodeType = node[1].getType(); + if(!nodeType.isBoolean()){ Node skolem = nodeManager->mkVar(node.getType()); Node newAssertion = @@ -112,6 +111,13 @@ Node TheoryEngine::removeITEs(TNode node) { nodeManager->mkNode(kind::EQUAL, skolem, node[2])); nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem); + if(debugTagIsOn("ite")){ + Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])" + << "->" + << "["<<newAssertion.getId() << "," << newAssertion << "]" + << endl; + } + Node preprocessed = rewrite(newAssertion); d_propEngine->assertFormula(preprocessed); |