CVC4 Ожидая максимум 3 аргумента для оператора 'ITE', найдено 5

Question

При вводе следующий файл cvc4, я получаю следующее сообщение об ошибке:

(error "Parse Error: <stdin>:11.221: Expecting at most 3 arguments for operator 'ITE', found 5") 

Файл test.txt был:

(declare-fun start!1() Bool) 

(assert start!1) 

(declare-fun lt!2() String) 

(declare-datatypes() ((JValue!1 (JInt!1 (v!75 (_ BitVec 32))) (JString!1 (v!76 String))))) 

(declare-fun a!0() JValue!1) 

(assert (=> start!1 (not (= lt!2 (ite false "" (ite (and (is-JString!1 a!0) (= (v!76 a!0) "")) """""" (ite (and (is-JInt!1 a!0) (= (v!75 a!0) #x00000000)) "0" (ite (and (is-JString!1 a!0) (= (v!76 a!0) "a")) """a""" lt!2)))))))) 

Командная строка:

cat test.txt | cvc4.exe 

Answer 1

мне нужно добавить опцию --lang smt2.5 для формата поддержки доу с помощью нового стандарта.

Итак:

cat test.txt | cvc4.exe --lang smt2.5