Parse error with CVC4 1.8

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless

Apache License 2.0

88 stars 20 forks source link

Parse error with CVC4 1.8 #110

Closed romac closed 3 years ago

romac commented 5 years ago

$ cvc4 --version
This is CVC4 version 1.8-prerelease [git master 7988675c]

With CVC4 above, every benchmark I have thrown to Inox has yielded:

Internal solver error in cvc4: Solver encountered exception: smtlib.parser.Parser$UnexpectedTokenException: Unexpected token at position: (9, 1). Expected: [OParen]. Found: unsat

I am unable to build latest CVC4 master at the moment, so I only tested with commit 7988675c.

samarion commented 3 years ago

@jad-hamza: is this now fixed with your CVC4 compatibility changes?

jad-hamza commented 3 years ago

Yes I think so, I had a similar error before removing the --rewrite-divk option which doesn't exist in CVC4 1.8 https://github.com/epfl-lara/inox/pull/132/files#diff-9a7682bc5396150985461a8eb80f16fbb3b5f8bd82ff28c3ec66918490226110L27

samarion commented 3 years ago

Marking as fixed after Jad's changes (thanks!)