diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 3e0278237..5245b9685 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -496,7 +496,6 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); if (arity == 0 && !is_const_op(k)) { - UNREACHABLE(); m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } @@ -514,7 +513,6 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); if (num_args == 0 && !is_const_op(k)) { - UNREACHABLE(); m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index af6cd6b26..75b8f86d0 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -54,7 +54,6 @@ namespace opt { unsigned m_upper; unsigned m_lower; model_ref m_model; - unsigned m_num_steps; imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft): m(m), @@ -64,8 +63,7 @@ namespace opt { m_orig_soft(soft), m_aux(m), m_upper(0), - m_lower(0), - m_num_steps(0) + m_lower(0) { m_upper = m_soft.size() + 1; m_assignment.resize(m_soft.size(), false);