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);
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");