diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index d01b8371b..f65462d1b 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -501,13 +501,17 @@ 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 (arity != r->get_arity()) {
-            m_manager->raise_exception("declared arity mismatches supplied arity");
-            return 0;            
+            if (r->get_info()->is_associative())
+                arity = r->get_arity();
+            else {
+                m_manager->raise_exception("declared arity mismatches supplied arity");
+                return 0;
+            }
         }
         for (unsigned i = 0; i < arity; ++i) {
             if (domain[i] != r->get_domain(i)) {
                 m_manager->raise_exception("declared sorts do not match supplied sorts");
-                return 0;            
+                return 0;
             }
         }
         return r;
@@ -596,15 +600,27 @@ 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;            
+            if (r->get_info()->is_associative()) {
+                sort * fs = r->get_domain(0);
+                for (unsigned i = 0; i < num_args; ++i) {
+                    if (m.get_sort(args[i]) != fs) {
+                        m_manager->raise_exception("declared sorts do not match supplied sorts");
+                        return 0;
+                    }
+                }
+                return r;
+            }
+            else {
+                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 0;
             }
         }
         return r;