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
332 stars 62 forks source link

support for >2 arity bxnor #61

Closed TrevorHansen closed 5 years ago

TrevorHansen commented 5 years ago

I think this should parse because bvxnor is left-associative:

(assert (= (bvxnor #b0 #b0 #b0) (bvnot (bvxor #b0 #b0 #b0))))

That said, bvxnor is hardly used.

mpreiner commented 5 years ago

Hi Trevor,

Thanks for the report! We'll change that in the parser accordingly.