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

debugging maxres bug report

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-16 11:22:58 -07:00
parent 0520d1a1f6
commit c64321c2e4
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/opt/maxres.cpp
View file

@ -781,9 +781,8 @@ public:
bool is_true(expr_ref_vector const& es) {
unsigned i = 0;
for (; i < es.size() && is_true(es[i]); ++i) { }
CTRACE("opt", i < es.size(), tout << mk_pp(es[i], m) << "\n";
model_smt2_pp(tout, m, *m_model, 0);
);
CTRACE("opt_bug", i < es.size(), tout << mk_pp(es[i], m) << "\n";
model_smt2_pp(tout, m, *m_model, 0););
return i == es.size();
}