mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

bug fix. Handle unknown without model (#4443)

Browse source
This commit is contained in:
Hari Govind V K 2020-05-22 13:12:42 -04:00 • committed by GitHub
parent 9eedd4ecd6
commit b7d7ff38cb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_context.cpp
View file

@ -3491,7 +3491,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r,
reach_pred_used, num_reuse_reach);
if (model) model->set_model_completion(false);
if (res == l_undef) res = handle_unknown(n, r, *model);
if (res == l_undef && model) res = handle_unknown(n, r, *model);
checkpoint ();
IF_VERBOSE (1, verbose_stream () << "." << std::flush;);