Description
lower_byte_operators (in expr_lowering.h) uses a pre-order visit strategy -- that is, remove byte ops from child expressions before removing this byte operator. By contrast the SMT2 backend (prior to #4379) used a post-order strategy: it called lower_byte_extract or lower_byte_update on each expression as it was found and then recursed over the result, lowering the parent operation before the child.
While these might have different results for various reasons, their meaning should be the same. However test cbmc/Pointer_byte_extract5 varies, failing more assertions (spuriously) when a preorder strategy is used.
To reproduce: compare this branch (https://github.com/smowton/cbmc/tree/smowton/wip/smt2-lower-byte-update-broken), which uses a preorder visit, with develop, which uses postorder. Running cbmc/Pointer_byte_extract5/no-simplify.desc should reveal that develop can only fail one assertion, as intended, while the WIP branch can fail two extra assertions.