From 27fa7077a62091937c5bd98f99fcddaf693f2f14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Apr 2014 09:22:31 +0200 Subject: [PATCH] fix compiler warnings/errors reported by Robert White Signed-off-by: Nikolaj Bjorner --- src/opt/pb_sls.cpp | 6 +++--- src/tactic/sls/bvsls_opt_engine.h | 11 ++++++++++- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index 0fe17a29a..c62c79c6a 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -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) { diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h index 75216c49e..64a366d73 100644 --- a/src/tactic/sls/bvsls_opt_engine.h +++ b/src/tactic/sls/bvsls_opt_engine.h @@ -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 \ No newline at end of file +#endif