3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-08 10:07:59 +00:00

try not to fail in add_sgn_inv_leading_coeff_for

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-10 16:26:04 -10:00
parent 0281ffc905
commit 3e29045b68

View file

@ -586,7 +586,7 @@ namespace nlsat {
return;
}
// All coefficients vanish at the sample, so delineability cannot be established.
fail();
// fail();
}
// Extracted helper: check preconditions for an_del property; returns true if ok, false otherwise.