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

fix #4231

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-07 10:34:38 -07:00
parent eda2eb5124
commit aa3749f678
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_context.cpp
View file

@ -3646,7 +3646,10 @@ namespace smt {
if (status == l_true && m_qmanager->has_quantifiers()) { if (status == l_true && m_qmanager->has_quantifiers()) {
// possible outcomes DONE l_true, DONE l_undef, CONTINUE // possible outcomes DONE l_true, DONE l_undef, CONTINUE
mk_proto_model(); mk_proto_model();
quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); quantifier_manager::check_model_result cmr = quantifier_manager::UNKNOWN;
if (m_proto_model.get()) {
cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
}
switch (cmr) { switch (cmr) {
case quantifier_manager::SAT: case quantifier_manager::SAT:
return false; return false;