mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-13 04:13:01 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-08 07:37:39 -07:00
parent eb6758bd6f
commit 7f7658cc52
3 changed files with 107 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_solver.cpp
View file

@ -2523,8 +2523,8 @@ namespace nlsat {
resolve_clause(b, *(jst.get_clause()));
break;
case justification::LAZY:
m_apply_lws = m_stats.m_conflicts == 2;
resolve_lazy_justification(b, *(jst.get_lazy()));
resolve_lazy_justification(b, *(jst.get_lazy()));
break;
case justification::DECISION:
SASSERT(m_num_marks == 0);