I am doing exercise 2 of Verfi_stack. I got stuck because of the tactic `forward_if`

.

The subgoal is illustrated as follows:

```
1 subgoal
Espec : OracleKind
p : val
i : Z
il : list Z
gv : globals
Delta_specs := abbreviate : Maps.PTree.t funspec
Delta := abbreviate : tycontext
H : Int.min_signed <= i <= Int.max_signed
POSTCONDITION := abbreviate : ret_assert
MORE_COMMANDS := abbreviate : statement
H0 : eq_dec nullval nullval = left eq_refl
```

```
semax Delta
(PROP ( )
LOCAL (temp _q nullval; gvars gv;
temp _p p; temp _i (Vint (Int.repr i)))
SEP (mem_mgr gv; emp; stack il p))
(if (!_q) {
_exit((1));
}
MORE_COMMANDS) POSTCONDITION
```

The `hint`

shows: `Hint: try 'forward_if', which may inform you that you need to supply a postcondition`

.

So, I was trying to use `forward_if`

to forward `if`

block, that is, `(if(!_q)) {_exit((1))}`

. But it didn’t work, showing `No matching clauses for match`

.

I did check how to use this tactic in Verifiable C, but I am still not having a clue about how to use it to solve this subgoal.

Thank you!

.