mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Fixed model-converter segfault in ::check_sat. Relates to #881

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-02-05 17:53:44 +00:00
parent 54280b6cc5
commit e4411265ea
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/tactic.cpp
View file

@ -220,7 +220,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
else {
if (models_enabled) {
model_converter2model(m, mc.get(), md);
(*mc)(labels, 0);
if (mc)
(*mc)(labels, 0);
}
reason_unknown = "incomplete";
return l_undef;