final IntExpression ians = (op!=ExprQt.Op.SUM) ? null : cint(sub) ;
for(Decl d: xvars) for(ExprHasName v: d.names) env.remove((ExprVar)v);
if (op==ExprQt.Op.COMPREHENSION) return ans.comprehension(dd); // guards.size()==0, since each var has to be unary
if (op==ExprQt.Op.SUM) return ians.sum(dd); // guards.size()==0, since each var has to be unary
if (op==ExprQt.Op.SOME) {
if (guards.size()==0) return ans.forSome(dd);
guards.add(ans);
return Formula.and(guards).forSome(dd);
} else {
if (guards.size()==0) return ans.forAll(dd);
return Formula.and(guards).implies(ans).forAll(dd);