From 46a5aeaef1c0ed393c4595b72fb7805ff3056585 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2015 14:10:22 -0700 Subject: [PATCH] improve type checking and reporting, fixes issue #116 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index b056ded36..37b339ddb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -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);