Search code examples
smtcvc4

cvc4 error with LANG_AUTO and antlr

I've built cvc4 from source according to their manual here. I ran make check which went perfect, then sudo make install. Then, I've tried running a simple example that works with z3:

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

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

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

But I get this error:

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

What am I doing wrong? Thanks!

Solution

  • It turns out I invoked it wrong from the command line. Here's what works:

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

    Which produces the following result:

    sat
((i 5) (j 4))