Redefined variables when branching on preprocessor flags

Conditionals that branch on a boolean variable marked as `@CIfDef` may extract to code that redefines variables.

```FStar
[@CIfDef]
assume val b : bool
assume val f : unit -> St UInt8.t

inline_for_extraction let g () =
if b then
let n = f () in
()

let test () =
g ();
g ()
```

extracts to

```C
void test()
{
#if DEBUG
uint8_t n1 = f();
#endif
#if DEBUG
uint8_t n1 = f();
#endif
}
```

which redefines `n1`. There should be an additional pass to generate unique names, or the variables could be defined in their own block.

Start with the extraction path that handles @CIfDef conditionals and emits the shown C declarations; the issue does not name a file or test. Reproduce the example and trace how each branch-local variable receives its name. Done means repeated calls no longer produce duplicate declarations in the generated C, while preserving the conditional behavior.

Written by the indexing model from the issue text.