message: Z3: use qe-light and 2 rounds of elim unconstrained vars
diff: @@ -344,7 +344,10 @@ void solver_init() {
  "propagate-values",
  "simplify",
  "elim-uncnstr",
  -// "qe2",
  + "qe-light",
  + "simplify",
  + "elim-uncnstr",
  + "qe-light",
  "simplify",
  "smt"
  };
  