diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 1079d43f6..bf6895abd 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -51,14 +51,18 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     expr* e = term;
     ctx.get_rewriter()(e, r);
     TRACE("user_propagate", tout << "add " << mk_bounded_pp(e, m) << "\n");
-    if (r != e) {
+    if (!is_ground(r)) {
+        if (m_add_expr_fresh.contains(term))
+            return;
+        m_add_expr_fresh.insert(term);
+        ctx.push_trail(insert_obj_trail(m_add_expr_fresh, term));
         r = m.mk_fresh_const("aux-expr", e->get_sort());
         expr_ref eq(m.mk_eq(r, e), m);
         ctx.assert_expr(eq);
         ctx.internalize_assertions();
-        e = r;
         ctx.mark_as_relevant(eq.get());
     }
+    e = r;
     enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h
index 5dbae59ed..c9409612e 100644
--- a/src/smt/theory_user_propagator.h
+++ b/src/smt/theory_user_propagator.h
@@ -88,6 +88,7 @@ namespace smt {
         lbool                  m_next_split_phase = l_undef;
         vector<expr_ref_vector> m_clauses_to_replay;
         unsigned                m_replay_qhead = 0;
+        obj_hashtable<expr>   m_add_expr_fresh;
 
         expr* var2expr(theory_var v) { return m_var2expr.get(v); }
         theory_var expr2var(expr* e) { check_defined(e); return m_expr2var[e->get_id()]; }
@@ -107,7 +108,6 @@ namespace smt {
 
     public:
         theory_user_propagator(context& ctx);
-        
         ~theory_user_propagator() override;
 
         /*