Merge pull request #4062 from tautschnig/byte-op-1

byte_extract lowering: lower newly introduced byte_extract expressions [depends-on: #4061, blocks: #2068]

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -289,7 +289,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
       tmp.type()=comp.type();
       tmp.offset()=new_offset;
 
-      s.add_to_operands(std::move(tmp));
+      s.add_to_operands(lower_byte_extract(tmp, ns));
     }
 
     if(!failed)

unit/solvers/lowering/byte_operators.cpp

@@ -162,9 +162,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
             const exprt lower_be = lower_byte_extract(be, ns);
             const exprt lower_be_s = simplify_expr(lower_be, ns);
 
-            // TODO: does not currently hold
-            // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_little_endian));
-            // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_big_endian));
+            REQUIRE(!has_subexpr(lower_be, ID_byte_extract_little_endian));
+            REQUIRE(!has_subexpr(lower_be, ID_byte_extract_big_endian));
             REQUIRE(lower_be.type() == be.type());
             // TODO: does not currently hold
             // REQUIRE(lower_be == r);