Redefined variables when branching on preprocessor flags

[s-zanella]

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

[@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

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.

[s-zanella]

I've seen a similar bug with variables redefined in different branches of a switch statement.