mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

ensure b_internalized

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-20 13:27:23 +01:00
parent a3d4e9a4e8
commit 7a8c969033
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_user_propagator.cpp
View file

@ -208,7 +208,14 @@ bool theory_user_propagator::internalize_term(app* term) {
ensure_enode(arg); ensure_enode(arg);
if (term->get_family_id() == get_id() && !ctx.e_internalized(term)) if (term->get_family_id() == get_id() && !ctx.e_internalized(term))
ctx.mk_enode(term, true, false, true); ctx.mk_enode(term, true, false, true);
unsigned v = add_expr(term); 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) if (m_created_eh)
m_created_eh(m_user_context, this, term, v); m_created_eh(m_user_context, this, term, v);
return true; return true;