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

Maybe a parsing bug? #161

Closed JoanEspasa closed 3 years ago

JoanEspasa commented 3 years ago

First at all, thanks for making an amazing solver!

I think I found a kinda simple bug. I minimized the instance that I'm generating to this:

(set-logic QF_BV)
(declare-fun x4 () Bool)
(declare-fun param_00020 () (_ BitVec 9))
(assert (= (or (= param_00020 #b000000001))  x4))

And the solver returns:

boolector: file.smt2:3:13: argument to 'or' missing

I'm using version 3.1.0. Z3 and Yices parse it correctly, so I guess having an or with only one operand its not a syntax error?

Thanks again 👍

aytey commented 3 years ago

This isn't a bug ... Z3 and Yices are just "more permissive" in the variant of SMTLIB2 they accept.

According to SMTLIB2, or (and other Boolean connectives such as and) are all arity >= 2. It just so happens that Z3/Yices/(some other solvers) accept the 1-arity variant.

aytey commented 3 years ago

See, e.g., https://github.com/Boolector/boolector/issues/119

mpreiner commented 3 years ago

As @andrewvaughanj mentioned this is not standard SMT-LIB.

JoanEspasa commented 3 years ago

Many thanks, I was not aware of that. Sorry for bothering you guys :)