Should we allow to create several symbols with identical name but different sort?

[kfriedberger]

Some solvers allow to create symbols (and UFs) with identical names and different sorts. We should discuss whether we want to avoid such inconsistencies and how to react when creating such a symbol. Currently, we support as much as each solver itself allows, if there is no conflict in our corresponding wrapper. This leaves a large gap between some solvers, which might be a problem when switching a solver in some user application.

This issue might be related to #171.

[PhilippWendler]

Should formulas could never be exported to SmtLib, right?

[kfriedberger]

Exporting is not the problem, because that is just a String representation. However, parsing such a query will (hopefully) always result in a crash.