mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

Bugfix for zero-extend.

Browse source 
Fixes #548
This commit is contained in:
Christoph M. Wintersteiger 2016-04-01 12:48:06 +01:00
parent dcca3a9bb1
commit dafda681b2
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/bv_decl_plugin.cpp
View file

@ -372,7 +372,8 @@ bool bv_decl_plugin::get_concat_size(unsigned arity, sort * const * domain, int
bool bv_decl_plugin::get_extend_size(unsigned num_parameters, parameter const * parameters, bool bv_decl_plugin::get_extend_size(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, int & result) { unsigned arity, sort * const * domain, int & result) {
int arg_sz; int arg_sz;
if (arity != 1 || num_parameters != 1 || !parameters[0].is_int() || !get_bv_size(domain[0], arg_sz)) { if (arity != 1 || !get_bv_size(domain[0], arg_sz) ||
num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
return false; return false;
} }
result = arg_sz + parameters[0].get_int(); result = arg_sz + parameters[0].get_int();