mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3416

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-19 08:54:08 -07:00
parent e075f38152
commit 31ff658f5e
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.cpp
View file

@ -2384,7 +2384,6 @@ namespace smt {
\warning This method will not invoke reset_cache_generation. \warning This method will not invoke reset_cache_generation.
*/ */
unsigned context::pop_scope_core(unsigned num_scopes) { unsigned context::pop_scope_core(unsigned num_scopes) {
unsigned units_to_reassert_lim; unsigned units_to_reassert_lim;
try { try {
@ -3871,7 +3870,6 @@ namespace smt {
final_check_status context::final_check() { final_check_status context::final_check() {
TRACE("final_check", tout << "final_check inconsistent: " << inconsistent() << "\n"; display(tout); display_normalized_enodes(tout);); TRACE("final_check", tout << "final_check inconsistent: " << inconsistent() << "\n"; display(tout); display_normalized_enodes(tout););
CASSERT("relevancy", check_relevancy()); CASSERT("relevancy", check_relevancy());
if (m_fparams.m_model_on_final_check) { if (m_fparams.m_model_on_final_check) {
mk_proto_model(); mk_proto_model();
@ -4458,6 +4456,11 @@ namespace smt {
bool context::update_model(bool refinalize) { bool context::update_model(bool refinalize) {
final_check_status fcs = FC_DONE; final_check_status fcs = FC_DONE;
if (refinalize) { if (refinalize) {
bool_var var;
lbool phase = l_undef;
m_case_split_queue->next_case_split(var, phase);
if (var != null_bool_var)
return false;
fcs = final_check(); fcs = final_check();
} }
TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";); TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);

1
src/smt/theory_pb.cpp
View file

@ -2172,6 +2172,7 @@ namespace smt {
TRACE("pb", display(tout << "validate: ", c, true); TRACE("pb", display(tout << "validate: ", c, true);
tout << "sum: " << sum << " " << maxsum << " "; tout << "sum: " << sum << " " << maxsum << " ";
tout << ctx.get_assignment(c.lit()) << "\n"; tout << ctx.get_assignment(c.lit()) << "\n";
ctx.display(tout);
); );
SASSERT(sum <= maxsum); SASSERT(sum <= maxsum);