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

limit the size of bit vectors

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-11 16:40:54 -07:00
parent 0ac462108f
commit 14ff768a63
5 changed files with 16 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/arith/bv2int_rewriter.cpp
View file

@ -17,12 +17,13 @@ Notes:
--*/
#include "tactic/arith/bv2int_rewriter.h"
#include "tactic/tactic_exception.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
void bv2int_rewriter_ctx::update_params(params_ref const& p) {
m_max_size = p.get_uint("max_bv_size", UINT_MAX);
m_max_size = p.get_uint("max_bv_size", m_max_size);
}
struct lt_rational {
@ -617,6 +618,9 @@ expr* bv2int_rewriter::mk_extend(unsigned sz, expr* b, bool is_signed) {
if (sz == 0) {
return b;
}
if (sz > m_ctx.get_max_num_bits()) {
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
rational r;
unsigned bv_sz;
if (is_signed) {