mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

push equality for #4740

Browse source 
https://github.com/Z3Prover/z3/issues/4740#issuecomment-711460353
This commit is contained in:
Nikolaj Bjorner 2020-11-09 13:08:46 -08:00
parent 3c9ada54b6
commit e955bd09e5
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_internalizer.cpp
View file

@ -982,6 +982,7 @@ namespace smt {
bool_var v = enode2bool_var(e); bool_var v = enode2bool_var(e);
assign(literal(v), mk_justification(eq_propagation_justification(e->get_arg(0), e->get_arg(1)))); assign(literal(v), mk_justification(eq_propagation_justification(e->get_arg(0), e->get_arg(1))));
e->m_cg = e; e->m_cg = e;
push_eq(e, m_true_enode, eq_justification());
} }
else { else {
if (cgc_enabled) { if (cgc_enabled) {