The refutation API in the SMTConstraintManager was a hack to allow us to create an SMT solver and verify the constraints; it was conceptually wrong from the start. Now, we don't actually need to use the SMTConstraintManager and can create an SMT object directly, add the constraints and check them.
While updating the Falsification visitor, I inlined the two functions that were used to collect the constraints and add them to the solver.
As a result of this patch, we could move the SMT API elsewhere and as it's not really dependent on the CSA anymore. Maybe we can create a new dir (utils/smt) for Z3 and future solvers?