add an exhaustivity parameter to Branch constructor in Machine Code to handle C switch default case optimization in case of a singleton enum

ast modifs and additional arrow_taint phase to retrieve which arrow "protects" / "taints" which variable

since the df optim backward optim has been disabled, elimination is in a fixpoint now so elim chains are taken into account

use ghost variables instead of existential variables to avoid read / write capture problems with variable reuse

Discussion w Xavier: replace this mechanism (fragile because of non-constructive witnesses) with a ghost-variables-based mechanism

hopefully those are less problematic since they actually exists in the program as variables

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)