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

(or) fails with single argument #70

Closed copy closed 4 years ago

copy commented 4 years ago

I'm generating smt2 formulas from machine code and in some cases a single-argument (or) comes up:

% echo '(assert (or true))' | boolector
boolector: <stdin>:1:10: argument to 'or' missing

It's just a minor issue that I can work around easily, but it would be nice if one didn't have to special-case this.

mpreiner commented 4 years ago

Hi Fabian, This is not SMT-LIB conform, it requires at least two arguments. I don't think that we want to support this.