From 7bb969ab52b5ce55bc5b03c0c66e7b6f84bc6ac8 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Sun, 27 Mar 2022 04:36:15 +0200
Subject: [PATCH] Fixed problem with registering bitvector functions (#5923)

---
 src/smt/smt_context.cpp            | 2 +-
 src/smt/smt_context.h              | 2 +-
 src/smt/theory_user_propagator.cpp | 8 ++++----
 src/smt/theory_user_propagator.h   | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a7946a67608..377ad1f2b75 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -206,7 +206,7 @@ namespace smt {
         ast_translation tr(src_ctx.m, m, false);
         for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) {
             app* e = src_ctx.m_user_propagator->get_expr(i);
-            m_user_propagator->add_expr(tr(e));
+            m_user_propagator->add_expr(tr(e), true);
         }
     }
 
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index f1b2514b171..ac2b0cfc8dc 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1729,7 +1729,7 @@ namespace smt {
         void user_propagate_register_expr(expr* e) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
-            m_user_propagator->add_expr(e);
+            m_user_propagator->add_expr(e, true);
         }
 
         void user_propagate_register_created(user_propagator::created_eh_t& r) {
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 3f5310ce528..08170d4eb54 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -39,7 +39,7 @@ void theory_user_propagator::force_push() {
     }
 }
 
-void theory_user_propagator::add_expr(expr* term) {
+void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     force_push();
     expr_ref r(m);
     expr* e = term;
@@ -52,7 +52,7 @@ void theory_user_propagator::add_expr(expr* term) {
         e = r;
         ctx.mark_as_relevant(eq.get());
     }
-    enode* n = ensure_enode(e);
+    enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
 
@@ -90,7 +90,7 @@ void theory_user_propagator::propagate_cb(
 }
 
 void theory_user_propagator::register_cb(expr* e) {
-    add_expr(e);
+    add_expr(e, true);
 }
 
 theory * theory_user_propagator::mk_fresh(context * new_ctx) {
@@ -243,7 +243,7 @@ bool theory_user_propagator::internalize_term(app* term)  {
     if (term->get_family_id() == get_id() && !ctx.e_internalized(term)) 
         ctx.mk_enode(term, true, false, true);
     
-    add_expr(term);
+    add_expr(term, false);
     
     if (!m_created_eh)
         throw default_exception("You have to register a created event handler for new terms if you track them");
diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h
index 1045feb0ac1..d3194a3fe63 100644
--- a/src/smt/theory_user_propagator.h
+++ b/src/smt/theory_user_propagator.h
@@ -110,7 +110,7 @@ namespace smt {
             m_fresh_eh     = fresh_eh;
         }
 
-        void add_expr(expr* e);
+        void add_expr(expr* e, bool ensure_enode);
 
         void register_final(user_propagator::final_eh_t& final_eh) { m_final_eh = final_eh; }
         void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }