mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

Add check bv size. Bit-vector size must be greater than zero (Thanks to David Cok)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-03 14:42:58 -08:00
parent 8480b27311
commit bc8277f10d
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/bv_decl_plugin.cpp
View file

@ -171,6 +171,9 @@ sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter c
m_manager->raise_exception("expecting one integer parameter to bit-vector sort"); m_manager->raise_exception("expecting one integer parameter to bit-vector sort");
} }
unsigned bv_size = parameters[0].get_int(); unsigned bv_size = parameters[0].get_int();
if (bv_size == 0) {
m_manager->raise_exception("bit-vector size must be greater than zero");
}
mk_bv_sort(bv_size); mk_bv_sort(bv_size);
return m_bv_sorts[bv_size]; return m_bv_sorts[bv_size];
} }