Simplify target 7 equivalence condition

GaloisInc / pate

Patches Assured up to Trace Equivalence

Other

15 stars 2 forks source link

Simplify target 7 equivalence condition #415

Closed jim-carciofini closed 1 month ago

jim-carciofini commented 1 month ago

With the latest Pate changes the form of the equivalence condition changed a bit and the simplifications that previously applied need to be extended. We are now getting:

notp(intle(18, sbvToInteger(readLE4(#x20002d14))))

We want:

18 > readLE4(#x20002d14)

jim-carciofini commented 1 month ago

@thebendavis , does this eq cond look good? If yes, please close the ticket.

thebendavis commented 1 month ago

Looks great, thanks!

Fixed in 44cae29c17ce35666588b44cbf8a5e0fbe1f9df5