mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix compiler warnings/errors reported by Robert White

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-04-23 09:22:31 +02:00
parent a5ec46b167
commit 27fa7077a6
2 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/pb_sls.cpp
View file

@ -586,7 +586,7 @@ namespace smt {
return result;
}
expr* x, *y;
if (m.is_eq(f, x, y) || m.is_iff(f, x, y)) {
if ((m.is_eq(f, x, y) && m.is_bool(x)) || m.is_iff(f, x, y)) {
literal a = mk_literal(x);
literal b = mk_literal(y);
literal result = mk_aux_literal(f);
@ -615,9 +615,9 @@ namespace smt {
m_clauses.push_back(cls);
m_orig_clauses.push_back(f);
return result;
}
}
IF_VERBOSE(0, verbose_stream() << "not handled: " << mk_pp(f, m) << "\n";);
return null_literal;
return mk_aux_literal(f);
}
bool compile_clause(expr* _f, clause& cls) {

11
src/tactic/sls/bvsls_opt_engine.h
View file

@ -39,6 +39,15 @@ public:
lbool is_sat;
expr_ref optimum;
optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {}
optimization_result& operator=(optimization_result const& other) {
is_sat = other.is_sat;
optimum = other.optimum;
return *this;
}
optimization_result(optimization_result const& other):
is_sat(other.is_sat),
optimum(other.optimum) {
}
};
optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true);
@ -70,4 +79,4 @@ protected:
bool randomize_wrt_hard();
};
#endif
#endif