diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 37b339ddb..d01b8371b 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -566,6 +566,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { + ast_manager& m = *m_manager; int bv_size; if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { // bv_size is filled in. @@ -589,7 +590,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); } else if (num_args == 0 || !get_bv_size(args[0], bv_size)) { - m_manager->raise_exception("operator is applied to arguments of the wrong sort"); + m.raise_exception("operator is applied to arguments of the wrong sort"); return 0; } func_decl * r = mk_func_decl(k, bv_size);