diff --git a/Project2.fst b/Project2.fst index 1535b81..92729bb 100644 --- a/Project2.fst +++ b/Project2.fst @@ -138,7 +138,8 @@ let step te cs = | (INPUT, stack') -> Next (Exec(((gas-1, pc+1, mem, input::stack'), (actor, input, code), gs) :: ps)) | (GAS, stack') -> Next (Exec(((gas-1, pc+1, mem, gas::stack'), (actor, input, code), gs)::ps)) | (JUMP i, stack') -> Next (Exec((((gas-1, i, mem, stack'), (actor, input, code), gs))::ps)) - | (JUMPI i, b::stack') -> magic () + | (JUMPI i, b::stack') -> let j = (if b = 0 then pc+1 else i) in + Next (Exec((((gas-1, j, mem, stack'), (actor, input, code), gs)) :: ps)) | (RETURN, v::stack') -> magic () | (STOP, stack') -> Next (Ter (HaltState gs 0 (gas-1)) ps) | (TIMESTAMP, stack') -> magic ()