mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Add code for rejecting bitvector constants of size 0

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-06-28 19:21:27 -07:00
parent 544dfde454
commit d9941c0ccc
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/bv_decl_plugin.cpp
View file

@ -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.