Restrict bvxnor to only allow two operands (was n-ary). (#5138)
authorAina Niemetz <aina.niemetz@gmail.com>
Sat, 26 Sep 2020 01:08:08 +0000 (18:08 -0700)
committerGitHub <noreply@github.com>
Sat, 26 Sep 2020 01:08:08 +0000 (18:08 -0700)
commit160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78
tree3f56f693cf842a099911ec9cb3bedbda688d4951
parentc59345b93b2ecf3552f5205b312c262a1ae5eab8
Restrict bvxnor to only allow two operands (was n-ary). (#5138)

Bit-vector operator bvxnor was previously mistakenly marked as
left-assoicative in SMT-LIB. This has recently been corrected in
SMT-LIB. We  now restrict bvxnor to only allow two operands in order to
avoid confusion about the semantics, since the behavior of n-ary
operands to bvxnor is now undefined in SMT-LIB.
NEWS
src/api/cvc4cpp.cpp
test/regress/regress0/parser/bv_arity_smt2.6.smt2