mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-12 11:54:07 +00:00
Code Activity

relax a too strong assert

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-10 13:24:52 -10:00
parent b8d9baa088
commit 850cc3e120
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_explain.cpp
View file

@ -1755,9 +1755,11 @@ namespace nlsat {
}
#ifdef Z3DEBUG
TRACE(nlsat, m_solver.display(tout, result.size(), result.data()) << "\n"; );
for (literal l : result) {
CTRACE(nlsat, l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
SASSERT(l_true == m_solver.value(l));
if (max_var(result.size(), result.data()) > 0) { // avoid checking something like that x0 = 0 & x0 > 0 with empty sample
for (literal l : result) {
CTRACE(nlsat, l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
SASSERT(l_true == m_solver.value(l));
}
}
#endif
break;