Fixed problem with registering bitvector functions (#5923)

Z3Prover · Mar 27, 2022 · 7bb969a · 7bb969a
1 parent 3828130
commit 7bb969a
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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; }