Establish a testing methodology for SMT-related code

[Kukovec]

This issue is meant to aggregate discussions regarding tests, which involve Z3SolverContext (or, more specifically, SMT constraints). In general, SMT constraints make unit testing difficult, because adding constraints mutates the internal state of the solver context, which doesn't lend itself well to testing.

Please note any suggestions/comments/concerns below.