search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Parse error on UF with Array parameter #85

Closed dbueno closed 4 years ago

dbueno commented 4 years ago 
~/code/boolector3/build/bin/boolector parse-error.smt2 
boolector: parse-error.smt2:2:18: expected '_' at 'Array'

Unless I'm mistaken, the attached file is valid SMT2. parse-error.smt2.txt I'm using Boolector commit 30132cb434a4ec2ed2389eb904fde97ae09292f8.

Is this something Boolector currently supports?

mpreiner commented 4 years ago

It's valid SMT2, but Boolector does not support arrays as UF arguments.

dbueno commented 4 years ago

All right, thanks for confirming.