translation to SMTLib format + binary search tree proved

So the nice solution would be to instantiate a Z3Wrapper once at the beginning of rewriting and make checkQuery an instance method, then put the prelude in a field. The not-quite-nice solution would be to make it an instance method but make the class a singleton and create a static deprecated method `instance` which returns a Z3Wrapper. I am fine with you doing whichever is easier for now. I am in the process of refactoring to remove static methods and so forth, and it wouldn't be too much of a hardship for me to do this later when I get to the Java backend instead of making you do it now if it turns out to be tricky to achieve. It's your call.