wrose-example.py

import z3
s = z3.Solver()
bvp = 256
bvs = 2**bvp
balanceOf_signer = z3.BitVec('balanceOf_signer', bvp)
wad = z3.BitVec('wad', bvp)
reward = z3.BitVec('reward', bvp)
contract_balance = z3.Int('contract_balance') # z3.IntVal((10**18) * 4.48)

# Calculate balance of user after performing withdrawal
balanceOf_after = z3.BitVec('balanceOf_after', bvp)
s.add(balanceOf_after == balanceOf_signer - (wad + reward))

# Contract has a reasonable balance, say 500k ROSE
#s.add(contract_balance < z3.IntVal((10**18) * 500000))

# Must be able to perform 2 transfers
s.add(contract_balance >= z3.BV2Int(wad) + z3.BV2Int(reward))

# Contract current balance cannot exceed signer balance
s.add(balanceOf_signer < contract_balance)
#s.add(balanceOf_signer <= z3.BitVecVal((10**18) * 100))

# require(balanceOf[signer] >= wad + reward, "Insufficient Balance");
s.add(balanceOf_signer >= wad + reward)

s.add(balanceOf_after > balanceOf_signer)

s.check()
s.model()