diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 8b77244f9..f1c61619a 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -210,6 +210,10 @@ func_decl * bv_decl_plugin::mk_unary(ptr_vector<func_decl> & decls, decl_kind k,
 
 func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
                                     unsigned arity, sort * const * domain) {
+    if (bv_size == 0) {
+        m_manager->raise_exception("bit-vector size must be greater than zero");
+    }
+
     force_ptr_array_size(m_int2bv, bv_size + 1);
 
     if (arity != 1) {
@@ -415,6 +419,9 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
         return 0;
     }
     unsigned bv_size = parameters[1].get_int();
+    if (bv_size == 0) {
+        m_manager->raise_exception("bit-vector size must be greater than zero");
+    }
     // TODO: sign an error if the parameters[0] is out of range, that is, it is a value not in [0, 2^{bv_size})
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.