diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index c8985cfcd..57b4fd48b 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10656,7 +10656,7 @@ class UserPropagateBase:
         return Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
 
     #
-    # Propagation can only be invoked as during a fixed-callback.
+    # Propagation can only be invoked as during a fixed or final callback.
     # 
     def propagate(self, e, ids, eqs = []):
         num_fixed = len(ids)
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 14368328f..5a94b45d2 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1823,8 +1823,9 @@ namespace lp {
             }
         }
 
-        SASSERT(column_is_fixed(k));
-        if (j != k) {
+        CTRACE("arith", !column_is_fixed(k), print_terms(tout););
+        // SASSERT(column_is_fixed(k));
+        if (j != k && column_is_fixed(k)) {
             SASSERT(column_is_int(j) == column_is_int(k));
             equal_to_j = column_to_reported_index(k);
             TRACE("lar_solver", tout << "found equal column k = " << k <<
diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp
index 4ce19e12c..bfdcbb3ba 100644
--- a/src/smt/user_propagator.cpp
+++ b/src/smt/user_propagator.cpp
@@ -69,9 +69,12 @@ theory * user_propagator::mk_fresh(context * new_ctx) {
 final_check_status user_propagator::final_check_eh() {
     if (!(bool)m_final_eh)
         return FC_DONE;
+    force_push();
     unsigned sz = m_prop.size();
     m_final_eh(m_user_context, this);
-    return sz == m_prop.size() ? FC_DONE : FC_CONTINUE;
+    propagate();
+    bool done = (sz == m_prop.size()) && !ctx.inconsistent();
+    return done ? FC_DONE : FC_CONTINUE;
 }
 
 void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) {
@@ -122,11 +125,7 @@ void user_propagator::propagate() {
         for (auto const& p : prop.m_eqs)
             m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
         DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
-        IF_VERBOSE(5, 
-                   for (auto lit : m_lits) 
-                       verbose_stream() << lit << ":" << ctx.get_assignment(lit) << " ";
-                   verbose_stream() << "\n";);
-        
+
         if (m.is_false(prop.m_conseq)) {
             js = ctx.mk_justification(
                 ext_theory_conflict_justification(