Simplify byte extract: use lowering when expression is a constant

When none of the earlier simplification rules apply, rewrite the
expression to to apply simplification rules for arithmetic and logic
expressions.

Author: tautschnig

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$
 --

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<>