Implement switch statement for abstract values

Let v be an abstract value, then

switch(expr) { case 'a': {...; break;} case 'b': {...; break;} default: {...; break;} }

should not give an error but should have the same outcome as let v = expr; if (v === 'a') {...} else if (v === 'b') {...} else {...};

To tackle this task, first look at how the if statement is implemented for abstract conditions, then implement the switch case accordingly. Start with the simplest scenario, such as the one in the example above, then look at the complications that arise when a case falls through to the next case because there is no break in its code block.

Remember to update the path conditions and bear in mind that fall throughs complicate this.