Does jSMTLIB support Z3 strings and the various operations that can be performed on them, as shown [here](http://rise4fun.com/Z3/tutorialcontent/sequences)? Thanks, Josh
