translation to SMTLib format + binary search tree proved

make a TODO item? I will fix this performance issue together with indexing when I get back to the rewrite engine.