Unsolved nested overflow check

[Stevengre]

• Low priority: specific to this type of overflow check & cannot reduce a lot of patterns
• Related branch: https://github.com/runtimeverification/riscv-semantics/tree/jh/gt-32

Example

Bool2Word ( Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 4 , 8 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 4 , 8 ) , LE , Unsigned ) +Int Bool2Word ( 4294967295 <Int Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 0 , 4 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 0 , 4 ) , LE , Unsigned ) ) &Int 4294967295 <Int Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 4 , 8 ) , LE , Unsigned ) )