Fortress

The following scheme is implemented now: when the solver verdict is "sat" and the solver output contains errors, an exception is thrown (see isSat method at ru.ispras.fortress.expression.ExprUtils class).

This scheme is incomplete, because we cannot detect critical errors when the solver verdict is "unsat", for example.

So the following scheme should be implemented:

While parsing Z3 solver output, only those errors should be taken into account, that come before the solver verdict (sat, unsat, unknown).
Those errors are critical and the library should throw an appropriate exception.

Errors that come after the solver verdict (such errors appears every time we call "get-model" when the verdict is "unsat"), can be treated as warnings/non-critical or ignored (as you wish). There is no need to throw an exception on them.