I still am not following why it's necessary to do all of this functionality constructing checkSat and so forth here. It seems like the task of taking a side condition and replacing it with the code to check that side condition's satisfiability should be both extractable and already implemented elsewhere in this backend...