diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 53f058fb4..813c0cd1c 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -173,7 +173,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
         SASSERT(sz == out_bits.size());
         return;
     }
-    
+   
     if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
         SASSERT(sz == out_bits.size());
         return;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 97b8c999d..3c305723b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -883,11 +883,11 @@ namespace opt {
             bool neg;
             if (is_maxsat(fml, terms, weights, offset, neg, id, index)) {
                 objective& obj = m_objectives[index];
+
                 if (obj.m_type != O_MAXSMT) {
                     // change from maximize/minimize.
                     obj.m_id = id;
                     obj.m_type = O_MAXSMT;
-                    obj.m_weights.append(weights);
                     SASSERT(!m_maxsmts.contains(id));
                     add_maxsmt(id);
                 }
@@ -895,10 +895,13 @@ namespace opt {
                 SASSERT(obj.m_id == id);
                 obj.m_terms.reset();
                 obj.m_terms.append(terms);
+                obj.m_weights.reset();
+                obj.m_weights.append(weights);
                 obj.m_adjust_value.set_offset(offset);
                 obj.m_adjust_value.set_negate(neg);
                 m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
-                TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
+                TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";
+                      tout << terms << "\n";);
             }
             else if (is_maximize(fml, tr, orig_term, index)) {
                 purify(tr);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index e4f698914..94566c52b 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -471,12 +471,12 @@ namespace smt {
                 if (get_enode(v)->get_root() != get_enode(v2)->get_root()) {
                     SASSERT(get_bv_size(v) == get_bv_size(v2));
                     context & ctx      = get_context();
-                    justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
                     TRACE("fixed_var_eh", tout << "detected equality: v" << v << " = v" << v2 << "\n";
                           display_var(tout, v);
                           display_var(tout, v2););
                     m_stats.m_num_th2core_eq++;
                     add_fixed_eq(v, v2);
+                    justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
                     ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));                    
                     m_fixed_var_table.insert(key, v2);
                 }