mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove outdated comment
This commit is contained in:
parent
3f10933225
commit
251d49d133
|
@ -357,8 +357,6 @@ void eliminate_predicates::try_resolve(func_decl* p) {
|
|||
++num_neg;
|
||||
|
||||
TRACE("elim_predicates", tout << "try resolve " << p->get_name() << " " << num_pos << " " << num_neg << "\n");
|
||||
// TODO - probe for a definition
|
||||
// generally, probe for binary clause equivalences in binary implication graph
|
||||
|
||||
if (num_pos >= 4 && num_neg >= 2)
|
||||
return;
|
||||
|
|
Loading…
Reference in a new issue