Bad interaction between unused variable elimination and "let x = if ... in" hoisting

[R1kM]

This issue is based on the following comment in one of the HACL PRs: hacl-star/hacl-star#611 (comment)

The problematic code has the shape
let c = BN.bn_add args in Ghost.hide c, where bn_add is inline_for_extraction, and consists of an if_then_else statement.

After extraction, the resulting code has shape

uint64_t c1;
if e {
  use of c0
} else {
  use of c0
}
c1 = c0;
return;

As far as I understand, c1 is introduced as a temporary variable to handle let c = if e then .. else ... in, but is not used afterwards. It could be removed as part of an unused variable elimination pass.

[msprotz]

This might be improved by the recent fix to unused variable elimination. @R1kM can you tell me whether this is still valid?