Fix symbolic br_table

[chambart]

Avoids sharing choice_i32 between different choices...
Also improve the performances by swaping the overflow test and the select_i32
Reverts the maze test to use a br_table

[zapashcanon]

Fix #116

[chambart]

Rebased

[krtab]

Fix #116

I discovered recently that autofix messages MUST be in the initial message unfortunately. I've manually linked the issue.

[zapashcanon]

@filipeom, is there a way to remove some variables from a model ?

[filipeom]

@filipeom, is there a way to remove some variables from a model ?

We can request the solver for the specific variables we need. With the argument Solver.model ~symbols, we can provide a list of symbols for which we want a model. By default, the solver generates a model for all symbols present in the path condition.

I been meaning to improve the way we generate output for models and testsuites to include only the symbols created through our symbolic API. This would also eliminate these auxiliary choice_i32 variables from being printed. If you want, I can attempt to implement this in a separate PR 😃

[zapashcanon]

That would be nice, I created an issue so we don't forget about it, we can discuss it there