CVC4 1.7 support - Githubissues

nunchaku-inria / nunchaku

Model finder for higher-order logic

https://nunchaku-inria.github.io/nunchaku/

BSD 2-Clause "Simplified" License

42 stars 3 forks source link

CVC4 1.7 support #27

Closed samuelgruetter closed 5 years ago

samuelgruetter commented 5 years ago

I tried to run nunchaku on nunchaku-problems/tests/first_order.nun:

nunchaku tests/first_order.nun

but got

Error: in the interface to CVC4: non first-order list

Output of cvc4 --version:

This is CVC4 version 1.7-prerelease [git master 9168f325]
compiled with GCC version 8.1.1 20180712 (Red Hat 8.1.1-5)
on Oct 10 2018 01:26:41

With CVC4 version 1.5 it worked, though.

c-cube commented 5 years ago

Indeed, and I have similar errors with cvc4 1.6.

The flag -d 1 (or higher numbers) give more information including the output of cvc4.

It's probably related to the support of SMTLIB 2.6. cc @blanchette

c-cube commented 5 years ago

I fixed the datatype declaration syntax and the parsing of models. This particular issue should be fixed; if other problems pop please open another issue :slightly_smiling_face: