mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
parent
302c0d178c
commit
2b6dadcbc6
|
@ -801,7 +801,7 @@ namespace datalog {
|
|||
if (num_tail_unifiers == 1) {
|
||||
TRACE("dl", tout << "setting invalid: " << j << "\n";);
|
||||
valid.set(j, false);
|
||||
datalog::del_rule(m_mc, *r2, l_true);
|
||||
datalog::del_rule(m_mc, *r2, l_false);
|
||||
del_rule(r2, j);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue