mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
c846902285
commit
29a857e258
|
@ -1376,10 +1376,6 @@ bool core::patch_blocker(lpvar u, const monic& m) const {
|
|||
TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";);
|
||||
return true;
|
||||
}
|
||||
if (u == patched_j) {
|
||||
TRACE("nla_solver", tout << "u = " << u << " is equal to patched\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
bool ret = u == m.var() || m.contains_var(u);
|
||||
|
||||
|
|
Loading…
Reference in a new issue