3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-12 14:46:22 +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 1fe7359c7b
commit 845c0bfff0

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.