diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 2a880f918..a1a80df97 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -349,7 +349,7 @@ namespace sat {
         }
         bool nullify = p.lit() != null_literal && value(p.lit()) == l_true;
         if (nullify) {
-            IF_VERBOSE(10, display(verbose_stream() << "nullify tracking literal\n", p, true););
+            IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true););
             SASSERT(lvl(p.lit()) == 0);
             nullify_tracking_literal(p);
             init_watch(p, true);
@@ -374,7 +374,7 @@ namespace sat {
         if (p.k() == 1 && p.lit() == null_literal) {
             literal_vector lits(p.literals());
             s().mk_clause(lits.size(), lits.c_ptr(), p.learned());
-            IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
+            IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
             remove_constraint(p, "implies clause");
         }
         else if (true_val == 0 && num_false == 0) {
@@ -384,14 +384,14 @@ namespace sat {
         }
         else if (true_val >= p.k()) {
             if (p.lit() != null_literal) {
-                IF_VERBOSE(10, display(verbose_stream() << "assign true literal ", p, true););
+                IF_VERBOSE(100, display(verbose_stream() << "assign true literal ", p, true););
                 s().assign(p.lit(), justification());
             }        
             remove_constraint(p, "is true");
         }
         else if (slack + true_val < p.k()) {
             if (p.lit() != null_literal) {
-                IF_VERBOSE(10, display(verbose_stream() << "assign false literal ", p, true););
+                IF_VERBOSE(100, display(verbose_stream() << "assign false literal ", p, true););
                 s().assign(~p.lit(), justification());
             }
             else {
@@ -2877,7 +2877,7 @@ namespace sat {
     bool ba_solver::elim_pure(literal lit) {
         if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && 
             use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) {
-            IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";);
+            IF_VERBOSE(100, verbose_stream() << "pure literal: " << lit << "\n";);
             s().assign(lit, justification());
             return true;
         }
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 3719b5a6a..d0e70546b 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -61,7 +61,7 @@ public:
     /**
        \brief Retrieve set of parameters set on solver.
      */
-    virtual params_ref const& get_params() { return m_params; }
+    virtual params_ref const& get_params() const { return m_params; }
 
     /**
        \brief Store in \c r a description of the configuration
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index 33a8fcd46..22303f62a 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -134,6 +134,7 @@ public:
 
 private:
     void flush_assertions() const {
+        m_rewriter.updt_params(get_params());
         proof_ref proof(m);
         expr_ref fml1(m), fml(m);
         expr_ref_vector fmls(m);