diff --git a/regression/cbmc-library/memcpy-01/constant-propagation.desc b/regression/cbmc-library/memcpy-01/constant-propagation.desc index 86e9c33caf7..00e7f65afa1 100644 --- a/regression/cbmc-library/memcpy-01/constant-propagation.desc +++ b/regression/cbmc-library/memcpy-01/constant-propagation.desc @@ -1,7 +1,7 @@ CORE main.c ---show-vcc -main::1::m!0@1#2 = .*byte_extract_(big|little)_endian\(cast\(44, signedbv\[\d+\]\*\), 0, signedbv\[\d+\]\).* + +^Generated 1\d* VCC\(s\), 0 remaining after simplification$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 0b47a7cbf97..b52a738ffbb 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1976,10 +1976,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) // try to refine it down to extracting from a member or an index in an array auto subexpr = get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns); - if(!subexpr.has_value() || subexpr.value() == expr) - return unchanged(expr); + if(subexpr.has_value() && subexpr.value() != expr) + return changed(simplify_rec(subexpr.value())); // recursive call + + if(is_constantt(ns)(expr)) + return changed(simplify_rec(lower_byte_extract(expr, ns))); - return changed(simplify_rec(subexpr.value())); // recursive call + return unchanged(expr); } simplify_exprt::resultt<> diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index f4a9996eebd..67b3b9a7883 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -906,7 +906,14 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) .set_width( to_bitvector_type(eb_i.type()).get_width() + to_bitvector_type(eb_n.type()).get_width()); - opi = eb_merged; + if(expr.type().id() != eb_merged.type().id()) + { + bitvector_typet bt = to_bitvector_type(expr.type()); + bt.set_width(to_bitvector_type(eb_merged.type()).get_width()); + opi = simplify_typecast(typecast_exprt{eb_merged, bt}); + } + else + opi = eb_merged; // erase opn new_expr.operands().erase(new_expr.operands().begin() + i + 1); no_change = false;