From 7a8c969033f69c58af364a0c2438bc2bb412954d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 Jan 2022 13:27:23 +0100
Subject: [PATCH] ensure b_internalized
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_user_propagator.cpp | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 797441b2e..dc397432a 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -208,7 +208,14 @@ bool theory_user_propagator::internalize_term(app* term) {
ensure_enode(arg);
if (term->get_family_id() == get_id() && !ctx.e_internalized(term))
ctx.mk_enode(term, true, false, true);
+
unsigned v = add_expr(term);
+ if (m.is_bool(term)) {
+ bool_var bv = ctx.mk_bool_var(term);
+ ctx.set_var_theory(bv, get_id());
+ ctx.set_enode_flag(bv, true);
+ }
+
if (m_created_eh)
m_created_eh(m_user_context, this, term, v);
return true;