smt: fix bug in manual quant instantiation when expr doesn't have a given ty_%x var
MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -121,8 +121,10 @@ static expr preprocess(Transform &t, const set<expr> &qvars,
for (auto &e : instances) {
for (unsigned i = 0; i <= 2; ++i) {
expr newexpr = e.subst(var, nums[i]);
- if (newexpr.eq(e))
+ if (newexpr.eq(e)) {
+ instances2.emplace(move(newexpr));
break;
+ }
newexpr = newexpr.simplify();
if (newexpr.isFalse())

smt: fix bug in manual quant instantiation when expr doesn't have a given ty_%x var