fix integer vars in Z3str, fix length/size constraints
expose substr