mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

disable 'optimization' that led to wrong model'

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-15 02:40:52 +02:00
parent ac893e907f
commit 50f18a77af
4 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_solver.cpp
View file

@ -26,6 +26,7 @@ Notes:
#include "ast_pp.h"
#include "ast_smt_pp.h"
#include "pp_params.hpp"
#include "model_smt2_pp.h"
namespace opt {
@ -130,6 +131,7 @@ namespace opt {
smt::theory_var v = m_objective_vars[i];
m_objective_values[i] = get_optimizer().maximize(v);
m_context.get_context().update_model();
TRACE("opt", { model_ref mdl; get_model(mdl); model_smt2_pp(tout << "update model: ", m, *mdl, 0); });
}
void opt_solver::get_unsat_core(ptr_vector<expr> & r) {