mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 20:01:20 +00:00
Code Activity

reset m_conflict indicator on sls model

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-15 20:56:44 -08:00
parent 557c01a0e5
commit a941f5ae84
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

@ -3517,6 +3517,7 @@ namespace smt {
r = l_undef; r = l_undef;
if (r == l_undef && m_internal_completed == l_true && has_sls_model()) { if (r == l_undef && m_internal_completed == l_true && has_sls_model()) {
m_last_search_failure = OK; m_last_search_failure = OK;
m_conflict = null_b_justification;
r = l_true; r = l_true;
} }
m_internal_completed = l_false; m_internal_completed = l_false;