From d4dd608badd15221cd95da57ddc044f19e239fab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2015 14:11:31 -0700 Subject: [PATCH] improve type checking and reporting, fixes issue #116 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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);