Smart contracts are programs that are stored on a blockchain ledger with code immutable
after deployment. Thus, verifying the correct behavior of smart contracts before deployment
is vital. This paper demonstrates how a security vulnerability verification in a casino
smart contract can be transformed to non-blocking verification. To this end, the contract
is first modeled as interacting extended finite state machines (EFSM), with one EFSM for
each function. Modeling the security vulnerability as a condition in the EFSM system,
non-blocking verification reveals the system to be blocking. Investigating the
counterexample produced by the verification shows that a transfer that is refused by its
receiver may block the casino so that all remaining funds are forever locked into the
contract, thus revealing a severe vulnerability. It is then demonstrated how the same
technique can show the absence of this vulnerability, by verifying that the EFSM model
of an improved casino contract is indeed non-blocking.