From bc8277f10d1f12fc2a954ed8a49b5f46a3bc6257 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Feb 2013 14:42:58 -0800 Subject: [PATCH] Add check bv size. Bit-vector size must be greater than zero (Thanks to David Cok) Signed-off-by: Leonardo de Moura --- src/ast/bv_decl_plugin.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 9c5bccbc6..dcefe59c3 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -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"); } 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); return m_bv_sorts[bv_size]; }