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

save model from level 0, fix #1380

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-28 08:53:06 -08:00
parent 81ec5bae95
commit 103ce78c29
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/rewriter_def.h
View file

@ -190,6 +190,9 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
else if (m().is_false(cond)) {
arg = t->get_arg(2);
}
else {
std::cout << mk_ismt2_pp(cond, m()) << "\n";
}
if (arg) {
result_stack().shrink(fr.m_spos);
result_stack().push_back(arg);

5
src/qe/qsat.cpp
View file

@ -626,6 +626,9 @@ namespace qe {
SASSERT(validate_assumptions(*m_model.get(), asms));
SASSERT(validate_model(asms));
TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
if (m_level == 0) {
m_model_save = m_model;
}
push();
if (m_level == 1 && m_mode == qsat_maximize) {
maximize_model();
@ -1274,7 +1277,7 @@ namespace qe {
in->inc_depth();
result.push_back(in.get());
if (in->models_enabled()) {
mc = model2model_converter(m_model.get());
mc = model2model_converter(m_model_save.get());
mc = concat(m_pred_abs.fmc(), mc.get());
}
break;