Я установил Z3 версии 4.1, и я пытаюсь использовать его программно в Java-приложении. Мое приложение связывается с Z3 через ProcessBuilder. Версия Z3 проверяется как 4.1 с помощью аргумента командной строки / version.
Однако Z3 не принимает отрицательные константы как часть выражений. Когда я пытаюсь ввести отрицательные целые числа, я получаю следующее сообщение:
(error "line 4 column 31: unknown constant -1")
Это входные данные, которые я предоставляю Z3:
(push)
(declare-fun y () Int )
(define-fun x () Int y )
(assert (and (<= y 1000) (>= y -1) ) )
(assert (= x 42) )
(check-sat)
(pop)
Я использую следующие аргументы для создания экземпляра Z3:
Z3 /smt2 /in /t:2
Любая помощь приветствуется. Заранее спасибо.