mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-11 06:15:20 +02:00
parent 5fac396c2f
commit e05f5ef6d1
3 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/euf_internalize.cpp
View file

@ -139,6 +139,10 @@ namespace euf {
sat::literal lit2 = literal(v, false);
s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
if (relevancy_enabled()) {
add_root(~lit, lit2);
add_root(lit, ~lit2);
}
lit = lit2;
}