Improve some simplifications for booster

runtimeverification / kasmer-multiversx

Wasm semantics for the Elrond/MultiversX blockchain network

BSD 3-Clause "New" or "Revised" License

0 stars 0 forks source link

Closed jberthold closed 1 month ago

jberthold commented 1 month ago

added equivalents of some simplifications that use #Equals (those are ignored by booster)
added a trivial simplification for when boolToInt inside int64encoding is compared to a number > 1

Both were observed to cause missed simplification opportunities logged during proof execution (--log-context "request*,proxy,abort,detail)