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 /test/regress/regress0/parser | |
| 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 'test/regress/regress0/parser')
| -rw-r--r-- | test/regress/regress0/parser/bv_arity_smt2.6.smt2 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress0/parser/bv_arity_smt2.6.smt2 b/test/regress/regress0/parser/bv_arity_smt2.6.smt2 index 437d80f56..c8b159f3b 100644 --- a/test/regress/regress0/parser/bv_arity_smt2.6.smt2 +++ b/test/regress/regress0/parser/bv_arity_smt2.6.smt2 @@ -8,6 +8,5 @@ (not (= (bvmul x y z) (bvmul (bvmul x y) z))) (not (= (bvand x y z) (bvand (bvand x y) z))) (not (= (bvor x y z) (bvor (bvor x y) z))) - (not (= (bvxor x y z) (bvxor (bvxor x y) z))) - (not (= (bvxnor x y z) (bvxnor (bvxnor x y) z))))) + (not (= (bvxor x y z) (bvxor (bvxor x y) z))))) (check-sat) |