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

fix another bug reported by Mark Dunlop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-15 17:57:11 -08:00
parent 3298486136
commit b33f5f879e
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/opt/opt_context.cpp
View file

@ -854,7 +854,10 @@ namespace opt {
bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) { bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) {
if (!is_app(fml)) return false; if (!is_app(fml)) return false;
neg = false; neg = false;
orig_term = nullptr;
index = 0;
app* a = to_app(fml); app* a = to_app(fml);
if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) { if (m_objective_fns.find(a->get_decl(), index) && m_objectives[index].m_type == O_MAXSMT) {
for (unsigned i = 0; i < a->get_num_args(); ++i) { for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr_ref arg(a->get_arg(i), m); expr_ref arg(a->get_arg(i), m);
@ -996,13 +999,13 @@ namespace opt {
void context::from_fmls(expr_ref_vector const& fmls) { void context::from_fmls(expr_ref_vector const& fmls) {
TRACE("opt", tout << fmls << "\n";); TRACE("opt", tout << fmls << "\n";);
m_hard_constraints.reset(); m_hard_constraints.reset();
expr_ref orig_term(m);
for (expr * fml : fmls) { for (expr * fml : fmls) {
app_ref tr(m); app_ref tr(m);
expr_ref orig_term(m);
expr_ref_vector terms(m); expr_ref_vector terms(m);
vector<rational> weights; vector<rational> weights;
rational offset(0); rational offset(0);
unsigned index; unsigned index = 0;
symbol id; symbol id;
bool neg; bool neg;
if (is_maxsat(fml, terms, weights, offset, neg, id, orig_term, index)) { if (is_maxsat(fml, terms, weights, offset, neg, id, orig_term, index)) {