diff --git a/src/ast/simplifier/fpa_simplifier_plugin.cpp b/src/ast/simplifier/fpa_simplifier_plugin.cpp index 4aba9c76c..5775f1af0 100644 --- a/src/ast/simplifier/fpa_simplifier_plugin.cpp +++ b/src/ast/simplifier/fpa_simplifier_plugin.cpp @@ -24,16 +24,16 @@ m_rw(m) {} fpa_simplifier_plugin::~fpa_simplifier_plugin() {} bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); + set_reduce_invoked(); SASSERT(f->get_family_id() == get_family_id()); - return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE; + return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; } bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { set_reduce_invoked(); - return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE; + return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; }