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);