mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
10ad5bae21
commit
18a76ab82c
|
@ -140,8 +140,8 @@ namespace euf {
|
|||
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);
|
||||
add_aux(~lit, lit2);
|
||||
add_aux(lit, ~lit2);
|
||||
}
|
||||
lit = lit2;
|
||||
}
|
||||
|
|
|
@ -50,7 +50,7 @@ namespace q {
|
|||
}
|
||||
return;
|
||||
}
|
||||
if (exp.size() > 1 && is_exists(q) /* && l.sign() */) {
|
||||
if (exp.size() > 1 && is_exists(q) && l.sign()) {
|
||||
sat::literal_vector lits;
|
||||
lits.push_back(~l);
|
||||
for (expr* e : exp)
|
||||
|
|
Loading…
Reference in a new issue