diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 7c72419c1..6735272a1 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -62,8 +62,7 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
-
-
+    
     theory_var v = mk_var(n);
     m_var2expr.reserve(v + 1);
     m_var2expr[v] = term;
@@ -146,7 +145,7 @@ final_check_status theory_user_propagator::final_check_eh() {
         return FC_DONE;
     force_push();
     unsigned sz1 = m_prop.size();
-    unsigned sz2 = m_expr2var.size();
+    unsigned sz2 = get_num_vars();
     try {
         m_final_eh(m_user_context, this);
     }
@@ -157,7 +156,7 @@ final_check_status theory_user_propagator::final_check_eh() {
     propagate();
     CTRACE("user_propagate", ctx.inconsistent(), tout << "inconsistent\n");
     // check if it became inconsistent or something new was propagated/registered
-    bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
+    bool done = (sz1 == m_prop.size()) && (sz2 == get_num_vars()) && !ctx.inconsistent();
     return done ? FC_DONE : FC_CONTINUE;
 }