From dafda681b205927cc689fd3ee16e0142062dc775 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 1 Apr 2016 12:48:06 +0100 Subject: [PATCH] Bugfix for zero-extend. Fixes #548 --- src/ast/bv_decl_plugin.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index a64475c04..03b4fe637 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -370,9 +370,10 @@ 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, - unsigned arity, sort * const * domain, int & result) { + unsigned arity, sort * const * domain, int & result) { 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; } result = arg_sz + parameters[0].get_int();