diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-09-25 18:08:08 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-25 18:08:08 -0700 |
commit | 160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78 (patch) | |
tree | 3f56f693cf842a099911ec9cb3bedbda688d4951 /NEWS | |
parent | c59345b93b2ecf3552f5205b312c262a1ae5eab8 (diff) |
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.
Diffstat (limited to 'NEWS')
-rw-r--r-- | NEWS | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -29,6 +29,11 @@ Changes: SMT-LIB 2.6 semantics. * The `competition` build type includes the dependencies used for SMT-COMP by default. Note that this makes this build type produce GPL-licensed binaries. +* 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. Changes since 1.7 |