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

Fix in lackr_model_constructor.

Browse source
This commit is contained in:
Mikolas Janota 2016-02-26 14:48:00 +00:00
parent a2140085d6
commit ae9f369574
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ackermannization/lackr_model_constructor.cpp
View file

@ -34,11 +34,13 @@ struct lackr_model_constructor::imp {
, m_conflicts(conflicts) , m_conflicts(conflicts)
, m_b_rw(m) , m_b_rw(m)
, m_bv_rw(m) , m_bv_rw(m)
, m_evaluator(NULL)
, m_empty_model(m) , m_empty_model(m)
, m_ackr_helper(m) , m_ackr_helper(m)
{} {}
~imp() { ~imp() {
if (m_evaluator) dealloc(m_evaluator);
{ {
values2val_t::iterator i = m_values2val.begin(); values2val_t::iterator i = m_values2val.begin();
const values2val_t::iterator e = m_values2val.end(); const values2val_t::iterator e = m_values2val.end();
@ -136,7 +138,7 @@ struct lackr_model_constructor::imp {
conflict_list& m_conflicts; conflict_list& m_conflicts;
bool_rewriter m_b_rw; bool_rewriter m_b_rw;
bv_rewriter m_bv_rw; bv_rewriter m_bv_rw;
scoped_ptr<model_evaluator> m_evaluator; model_evaluator * m_evaluator;
model m_empty_model; model m_empty_model;
private: private:
struct val_info { expr * value; app * source_term; }; struct val_info { expr * value; app * source_term; };
@ -221,7 +223,11 @@ struct lackr_model_constructor::imp {
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
expr * val; expr * val;
const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app? const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); ); CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2) << '\n'; );
if (!b) {
// bailing out because args eval failed previously
return false;
}
TRACE("model_constructor", tout << TRACE("model_constructor", tout <<
"arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2) "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2)
<< " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; ); << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; );