ITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds. Fixed and added bug regression. Thanks Andrew Reynolds for the bug report!

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3c59b43e4..f8eece3df 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -310,6 +310,12 @@ Node TheoryEngine::removeITEs(TNode node) {
   }
   vector<Node> newChildren;
   bool somethingChanged = false;
+  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    // Make sure to push operator or it will be missing in new
+    // (reformed) node.  This was crashing on the very simple input
+    // "(f (ite c 0 1))"
+    newChildren.push_back(node.getOperator());
+  }
   for(TNode::const_iterator it = node.begin(), end = node.end();
       it != end;
       ++it) {