Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-ground...
authorMorgan Deters <mdeters@cs.nyu.edu>
Sat, 8 Mar 2014 20:33:46 +0000 (15:33 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Sat, 8 Mar 2014 20:33:46 +0000 (15:33 -0500)
src/theory/arith/arith_static_learner.cpp
src/util/ite_removal.cpp

index 3854188e00ee3a8a202b5849a7310e66e0375ac5..b9260c9069c19d859063224d58cfeb80a5569538 100644 (file)
@@ -109,6 +109,12 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
 
   switch(n.getKind()){
   case ITE:
+    if(n.hasBoundVar()) {
+      // Unsafe with non-ground ITEs; do nothing
+      Debug("arith::static") << "(potentially) non-ground ITE, ignoring..." << endl;
+      break;
+    }
+
     if(n[0].getKind() != EQUAL &&
        isRelationOperator(n[0].getKind())  ){
       iteMinMax(n, learned);
index 1ceedc6889eb8c7fac5936aba8995f564cf1d144..1b29f9ef8649b637da10741f46b7500f5b83f99b 100644 (file)
@@ -91,7 +91,6 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   if(node.getKind() == kind::ITE) {
     TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
-Debug("ite") << "CAN REMOVE ITE " << node << " BECAUSE " << inQuant << " " << node.hasBoundVar() << endl;
       Node skolem;
       // Make the skolem to represent the ITE
       skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");