mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
improve type checking and reporting, fixes issue #116
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
parent
168ea2e948
commit
46a5aeaef1
|
@ -594,6 +594,18 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
}
|
||||
func_decl * r = mk_func_decl(k, bv_size);
|
||||
if (r != 0) {
|
||||
if (num_args != r->get_arity()) {
|
||||
m.raise_exception("declared arity mismatches supplied arity");
|
||||
return 0;
|
||||
}
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
if (m.get_sort(args[i]) != r->get_domain(i)) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
|
||||
m.raise_exception(buffer.str().c_str());
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
|
||||
|
|
Loading…
Reference in a new issue