Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib