diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 033df7aa0..9a6cd0615 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -468,7 +468,14 @@ namespace smt {
         enode* n = get_enode(v);
         if (ctx.watches_fixed(n)) {
             expr_ref num(m_util.mk_numeral(val, m.get_sort(n->get_owner())), m);
-            ctx.assign_fixed(n, num, m_bits[v]);
+            literal_vector& lits = m_tmp_literals;
+            lits.reset();
+            for (literal b : m_bits[v]) {
+                if (ctx.get_assignment(b) == l_false)
+                    b.neg();
+                lits.push_back(b);
+            }
+            ctx.assign_fixed(n, num, lits);
         }
         unsigned sz = get_bv_size(v);
         value_sort_pair key(val, sz);
diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp
index 27adc950e..114d3fd7e 100644
--- a/src/smt/user_propagator.cpp
+++ b/src/smt/user_propagator.cpp
@@ -92,29 +92,24 @@ void user_propagator::propagate() {
         return;
     force_push();
     unsigned qhead = m_qhead;
-    literal_vector lits;
     enode_pair_vector eqs;
     justification* js;
     while (qhead < m_prop.size() && !ctx.inconsistent()) {
         auto const& prop = m_prop[qhead];
-        lits.reset();        
-        for (unsigned id : prop.m_ids) 
-            for (literal lit : m_id2justification[id]) {
-                if (ctx.get_assignment(lit) == l_false) 
-                    lit.neg();
-                lits.push_back(lit);
-            }
+        m_lits.reset();        
+        for (unsigned id : prop.m_ids)
+            m_lits.append(m_id2justification[id]);
         if (m.is_false(prop.m_conseq)) {
             js = ctx.mk_justification(
                 ext_theory_conflict_justification(
-                    get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), 0, nullptr));
+                    get_id(), ctx.get_region(), m_lits.size(), m_lits.c_ptr(), eqs.size(), eqs.c_ptr(), 0, nullptr));
             ctx.set_conflict(js);
         }
         else {
             literal lit = mk_literal(prop.m_conseq);
             js = ctx.mk_justification(
                 ext_theory_propagation_justification(
-                    get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit));
+                    get_id(), ctx.get_region(), m_lits.size(), m_lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit));
             ctx.assign(lit, js);
         }
         ++qhead;
diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h
index d905478f2..b27a6aa93 100644
--- a/src/smt/user_propagator.h
+++ b/src/smt/user_propagator.h
@@ -46,6 +46,7 @@ namespace smt {
         unsigned_vector        m_prop_lim;
         vector<literal_vector> m_id2justification;
         unsigned               m_num_scopes;
+        literal_vector         m_lits;
 
         void force_push();