mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix regression in o7.smt2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-08 22:27:47 -08:00
parent 9743c188da
commit 5db84575f6
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/opt/opt_context.cpp
View file

@ -896,7 +896,7 @@ namespace opt {
} }
mk_atomic(terms); mk_atomic(terms);
SASSERT(obj.m_id == id); SASSERT(obj.m_id == id);
obj.m_term = to_app(orig_term); obj.m_term = orig_term?to_app(orig_term):0;
obj.m_terms.reset(); obj.m_terms.reset();
obj.m_terms.append(terms); obj.m_terms.append(terms);
obj.m_weights.reset(); obj.m_weights.reset();
@ -940,6 +940,9 @@ namespace opt {
bool context::verify_model(unsigned index, model* md, rational const& _v) { bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r; rational r;
app_ref term = m_objectives[index].m_term; app_ref term = m_objectives[index].m_term;
if (!term) {
return true;
}
rational v = m_objectives[index].m_adjust_value(_v); rational v = m_objectives[index].m_adjust_value(_v);
expr_ref val(m); expr_ref val(m);
model_ref mdl = md; model_ref mdl = md;