带有cvc4和antlr的LANG_AUTO错误

Question

我根据他们的手动cvc4 这里从源代码中构建了这里。我运行了make check，它运行得很完美，然后是sudo make install。然后，我尝试运行一个适用于z3的简单示例：

(declare-const i Int)
(declare-const j Int)

(assert (= i 5))
(assert (= (+ i j) 9))

(check-sat)
(get-value (i j))

但我知道这个错误：

CVC4 Error:
internal error: unhandled language LANG_AUTO in AntlrInput::newInput

我做错了什么？谢谢!

Answer 1

结果，我从命令行调用了它。以下是起作用的原因：

cvc4 --quiet --produce-models --lang=smt2 ./example.txt

这将产生以下结果：

sat
((i 5) (j 4))