diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 4fa8c4074..4c81ab665 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -839,3 +839,13 @@ expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args)
 void th_rewriter::set_solver(expr_solver* solver) {
     m_imp->set_solver(solver);
 }
+
+
+bool th_rewriter::reduce_quantifier(quantifier * old_q, 
+                                    expr * new_body, 
+                                    expr * const * new_patterns, 
+                                    expr * const * new_no_patterns,
+                                    expr_ref & result,
+                                    proof_ref & result_pr) {
+    return m_imp->cfg().reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
+}
diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h
index 19a99f4d3..281c685f2 100644
--- a/src/ast/rewriter/th_rewriter.h
+++ b/src/ast/rewriter/th_rewriter.h
@@ -41,7 +41,7 @@ public:
     static void get_param_descrs(param_descrs & r);
     unsigned get_cache_size() const;
     unsigned get_num_steps() const;
-
+   
     void operator()(expr_ref& term);
     void operator()(expr * t, expr_ref & result);
     void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
@@ -49,6 +49,13 @@ public:
 
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args);
 
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr);
+
     void cleanup();
     void reset();
 
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 968aca51f..d2f14d9b4 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include "ast/rewriter/datatype_rewriter.h"
 #include "ast/rewriter/array_rewriter.h"
 #include "ast/rewriter/fpa_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
@@ -126,6 +127,17 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return false;
     }
 
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr) {
+        th_rewriter th(m);
+        return th.reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
+    }
+
+
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 81edb2c67..45ade8b46 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3332,7 +3332,7 @@ public:
             vi = m_theory_var2var_index[v];
             st = m_solver->maximize_term(vi, term_max);
         }
-        TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
+        TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << " " << term_max << "\n"););
         switch (st) {
         case lp::lp_status::OPTIMAL: {
             init_variable_values();