mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

fix #1577

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-03 17:49:57 -07:00
parent 3bc2213d54
commit f8e5d989bf
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/c++/z3++.h
View file

@ -2457,6 +2457,7 @@ namespace z3 {
} }
check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); } check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
check_result check(expr_vector const& asms) { check_result check(expr_vector const& asms) {
unsigned n = asms.size();
array<Z3_ast> _asms(n); array<Z3_ast> _asms(n);
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {
check_context(*this, asms[i]); check_context(*this, asms[i]);
@ -2467,7 +2468,7 @@ namespace z3 {
return to_check_result(r); return to_check_result(r);
} }
model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); } model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); } void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
expr lower(handle const& h) { expr lower(handle const& h) {
Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h()); Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());