translation to SMTLib format + binary search tree proved

There isn't any change in what can be translated, just the format is changed.