From 980772f40f15091ee3504121d3729da1d4fb8733 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 28 Jun 2026 15:58:36 -0700 Subject: [PATCH] nlsat: disable levelwise (lws) by default to fix QF_NIA SIGSEGV The experimental levelwise single-cell projection (nlsat.lws) crashes non-deterministically (~40%) with a SIGSEGV inside the root-function partition sort during conflict explanation. Default it off; the explain path falls back to add_all_coeffs projection, eliminating the crash. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/nlsat/nlsat_params.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 048fcf5218..f28f337b11 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -22,7 +22,7 @@ def_module_params('nlsat', ('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."), ('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."), ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), - ('lws', BOOL, True, "apply levelwise."), + ('lws', BOOL, False, "apply levelwise."), ('lws_spt_threshold', UINT, 4, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"), ('lws_witness_subs_lc', BOOL, True, "try substitute the non-nullified witness by the lc"), ('lws_witness_subs_disc', BOOL, True, "try substitute the non-nullified witness by the discriminant"),