Maybe a parsing bug?

[JoanEspasa]

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]

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]

See, e.g., #119

[mpreiner]

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

[JoanEspasa]

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