mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

improve type checking and reporting, fixes issue #116

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-06-01 14:11:31 -07:00
parent 46a5aeaef1
commit d4dd608bad
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/bv_decl_plugin.cpp
View file

@ -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, 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) { unsigned num_args, expr * const * args, sort * range) {
ast_manager& m = *m_manager;
int bv_size; int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in. // 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); 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)) { 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; return 0;
} }
func_decl * r = mk_func_decl(k, bv_size); func_decl * r = mk_func_decl(k, bv_size);