mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-19 19:43:11 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Valentin Promies 2026-03-06 14:30:22 +01:00
parent 3a995bbb0c
commit 77d81de03f
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/nlsat_explain.cpp
View file

@ -1733,7 +1733,7 @@ namespace nlsat {
// We call levelwise directly without normalize, simplify, elim_vanishing to preserve the original polynomials
var max_x = max_var(m_ps);
bool levelwise_ok = levelwise_single_cell(m_ps, max_x, m_cache, true);
bool levelwise_ok = levelwise_single_cell(m_ps, max_x+1, m_cache, true); // max_x+1 because we have a full sample
SASSERT(levelwise_ok);
m_solver.record_levelwise_result(levelwise_ok);