In some cases, such for as the binary here (regardless of whether BAP or GTIRB/ASLp are used), initial memory isn't consolidated into 64-bit accesses and remains represented as 8-bit accesses in the Boogie output, which causes the output file to be impractically large. I have not yet investigated why.
In some cases, such for as the binary here (regardless of whether BAP or GTIRB/ASLp are used), initial memory isn't consolidated into 64-bit accesses and remains represented as 8-bit accesses in the Boogie output, which causes the output file to be impractically large. I have not yet investigated why.