Равенство / отчетливость
Вы можете сравнить на равенство, используя =; другой специальный синтаксис не требуется:
(= a b)
Обратите внимание, что это работает одинаково для всех типов в SMTLib, а не только для строк. Для отрицания вы можете либо отменить результат, либо использовать distinct:
(not (= a b))
(distinct a b)
Преимущество distinct заключается в том, что он может принимать любое количество параметров и проверяет парное неравенство, то есть все аргументы отличаются друг от друга.
Лексикографические сравнения
Согласно http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml, строки поддерживают лексические сравнения через str.<=. К сожалению, связанная теория все еще находится в черновом варианте, и, насколько мне известно, ни Z3, ни какой-либо другой SMT-решатель (в частности CVC4) пока не поддерживают эту операцию.