diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h
index 8a1c62347..0bc6b21b4 100644
--- a/src/ast/converters/generic_model_converter.h
+++ b/src/ast/converters/generic_model_converter.h
@@ -68,6 +68,8 @@ public:
     void get_units(obj_map<expr, bool>& units) override;
 
     vector<entry> const& entries() const { return m_entries; }
+
+    void reset() { m_entries.reset(); }
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 64ecc5f53..db87cd008 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -555,7 +555,6 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
             result = m.mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2));
         else if (r1 < r2) 
             result = m.mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2));
-        verbose_stream() << result << "\n";
         return BR_REWRITE2;
     }
         
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index c7cf2d11c..260f01974 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -426,7 +426,7 @@ void elim_unconstrained::reduce() {
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
-    for (unsigned rounds = 0; m_created_compound && rounds < 1; ++rounds) {
+    for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) {
         m_created_compound = false;
         init_nodes();
         eliminate();
@@ -434,6 +434,7 @@ void elim_unconstrained::reduce() {
         vector<dependent_expr> old_fmls;
         assert_normalized(old_fmls);
         update_model_trail(*mc, old_fmls);
+        mc->reset();
     }
 
 }