search

runtimeverification / mx-semantics

6 stars 1 forks source link

Make `checkBool` a constructor #278

Closed bbyalcinkaya closed 1 month ago

bbyalcinkaya commented 1 month ago

This PR addresses the recent failure in the swap proof. The backend fails to evaluate a checkBool expression, leaving an unevaluated expression in the <commands> cell and creating too many branches. To resolve this, checkBool has been refactored from a function that returns a K sequence (.K or #exception()) to an InternalCmd constructor.

ehildenb commented 1 month ago

@bbyalcinkaya please include a description of the change, including why it's needed. Especially if you can post performance numbers for it.