Мягкие / жесткие ограничения в Z3

Как выразить мягкие и жесткие ограничения в Z3? Из API я знаю, что могут быть предположения (мягкие ограничения), но я не могу выразить это при использовании инструмента командной строки. Я вызываю его с помощью z3 / smt2 / si