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

fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-04 22:35:02 +00:00
parent 768bb84798
commit 2a65503235
3 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -173,7 +173,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
SASSERT(sz == out_bits.size());
return;
}
if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
SASSERT(sz == out_bits.size());
return;

7
src/opt/opt_context.cpp
View file

@ -883,11 +883,11 @@ namespace opt {
bool neg;
if (is_maxsat(fml, terms, weights, offset, neg, id, index)) {
objective& obj = m_objectives[index];
if (obj.m_type != O_MAXSMT) {
// change from maximize/minimize.
obj.m_id = id;
obj.m_type = O_MAXSMT;
obj.m_weights.append(weights);
SASSERT(!m_maxsmts.contains(id));
add_maxsmt(id);
}
@ -895,10 +895,13 @@ namespace opt {
SASSERT(obj.m_id == id);
obj.m_terms.reset();
obj.m_terms.append(terms);
obj.m_weights.reset();
obj.m_weights.append(weights);
obj.m_adjust_value.set_offset(offset);
obj.m_adjust_value.set_negate(neg);
m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";
tout << terms << "\n";);
}
else if (is_maximize(fml, tr, orig_term, index)) {
purify(tr);

2
src/smt/theory_bv.cpp
View file

@ -471,12 +471,12 @@ namespace smt {
if (get_enode(v)->get_root() != get_enode(v2)->get_root()) {
SASSERT(get_bv_size(v) == get_bv_size(v2));
context & ctx = get_context();
justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
TRACE("fixed_var_eh", tout << "detected equality: v" << v << " = v" << v2 << "\n";
display_var(tout, v);
display_var(tout, v2););
m_stats.m_num_th2core_eq++;
add_fixed_eq(v, v2);
justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
m_fixed_var_table.insert(key, v2);
}