diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 08cd8d9a2..188e3a416 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -7,6 +7,7 @@ def_module_params('opt',
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('print_model', BOOL, False, 'display model for satisfiable constraints'),
+                          ('print_all_models', BOOL, False, 'display all intermediary models for satisfiable constraints'),
                           ('debug_conflict', BOOL, False, 'debug conflict resolution'),
                           ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'iwmax' (iterative), 'bwmax' (bisection)"),
                           ('elim_01', BOOL, True, 'eliminate 01 variables')
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index b5c53c3be..93fa0c22f 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -423,13 +423,14 @@ namespace opt {
         rational         m_lower;
         model_ref        m_model;
         symbol           m_engine;
+        bool             m_print_all_models;
         volatile bool    m_cancel;
         params_ref       m_params;
         opt_solver       m_solver;
         scoped_ptr<imp>  m_imp;
 
         imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft_constraints, vector<rational> const& weights):
-            m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_cancel(false), 
+            m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_print_all_models(false), m_cancel(false), 
             m_solver(m, m_params, symbol("bound"))
         {
             m_assignment.resize(m_soft.size(), false);
@@ -533,7 +534,8 @@ namespace opt {
                 }
                 if (is_sat == l_true) {
                     if (wth().is_optimal()) {
-                        s.get_model(m_model);
+                        m_upper = wth().get_min_cost();
+                        updt_model(s);
                     }
                     expr_ref fml = wth().mk_block();
                     s.assert_expr(fml);
@@ -776,8 +778,8 @@ namespace opt {
                     is_sat = l_undef;
                 }
                 if (is_sat == l_true) {
-                    s.get_model(m_model);
                     m_upper = m_lower;
+                    updt_model(s);
                     for (unsigned i = 0; i < block.size(); ++i) {
                         VERIFY(m_model->eval(block[i].get(), val));
                         m_assignment[i] = m.is_false(val);
@@ -904,8 +906,8 @@ namespace opt {
                     return l_undef;
                 }
                 if (is_sat == l_true && wmax.is_zero()) {
-                    s.get_model(m_model);
                     m_upper = m_lower;
+                    updt_model(s);
                     for (unsigned i = 0; i < block.size(); ++i) {
                         VERIFY(m_model->eval(block[i].get(), val));
                         m_assignment[i] = m.is_false(val);
@@ -1059,12 +1061,23 @@ namespace opt {
         void updt_params(params_ref& p) {
             opt_params _p(p);
             m_engine = _p.wmaxsat_engine();        
+            m_print_all_models = _p.print_all_models();
             m_solver.updt_params(p);
             if (m_imp) {
                 m_imp->updt_params(p);
             }
         }
 
+        void updt_model(solver& s) {
+            s.get_model(m_model);
+            if (m_print_all_models) {
+                std::cout << "[" << m_lower << ":" << m_upper << "]\n";
+                std::cout << "(model " << std::endl;
+                model_smt2_pp(std::cout, m, *(m_model.get()), 2);
+                std::cout << ")" << std::endl;                 
+            }
+        }
+
         lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) {
             lbool is_sat = l_true;
             tactic_ref tac1 = mk_simplify_tactic(m);
@@ -1097,7 +1110,7 @@ namespace opt {
                 }
                 is_sat = m_solver.check_sat_core(0, 0);
                 if (l_true == is_sat && !m_cancel) {
-                    m_solver.get_model(m_model);
+                    updt_model(m_solver);
                     if (mc && m_model) (*mc)(m_model, 0);
                     IF_VERBOSE(2, 
                                g->display(verbose_stream() << "goal:\n");
@@ -1178,7 +1191,7 @@ namespace opt {
                 switch(is_sat) {
                 case l_true: {
                     if (wth().is_optimal()) {
-                        s.get_model(m_model);
+                        updt_model(s);
                     }
                     expr_ref fml = wth().mk_block();
                     s.assert_expr(fml);
diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp
index e6c345734..6a2c2cb2a 100644
--- a/src/tactic/arith/elim01_tactic.cpp
+++ b/src/tactic/arith/elim01_tactic.cpp
@@ -127,7 +127,7 @@ public:
     elim01_tactic(ast_manager & _m, params_ref const & p):
         m(_m),
         a(m),
-        m_max_hi_default(8),
+        m_max_hi_default(1),
         m_max_hi(rational(m_max_hi_default)) {
     }