From d9941c0ccc871881d4bbc1625bfdc005d4618ae8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Jun 2013 19:21:27 -0700 Subject: [PATCH] Add code for rejecting bitvector constants of size 0 Signed-off-by: Leonardo de Moura --- src/ast/bv_decl_plugin.cpp | 7 +++++++ 1 file changed, 7 insertions(+) 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 & 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.