Improve the parser for models returned by SMT solvers
The model parser behaves unexpectedly when encountering values whose name contains parentheses, which may happen for values introduced by the prover (that begin with @
), such as in:
(define-fun x_vc_constant () (poly_map Int Int) (as @(poly_map Int Int)_0 (poly_map Int Int)))
Since the parser also throws away most exceptions, this was both hard to detect and to inspect. The fix for this is simple, but the parser should be strengthened.
In the future we might consider using an external library for this, for example Dolmen.