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 /src/api/cvc4cpp.cpp | |
| 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 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 08beec35a..6ed8855e4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3145,7 +3145,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const if (echildren.size() > 2) { if (kind == INTS_DIVISION || kind == XOR || kind == MINUS - || kind == DIVISION || kind == BITVECTOR_XNOR || kind == HO_APPLY) + || kind == DIVISION || kind == HO_APPLY) { // left-associative, but CVC4 internally only supports 2 args res = d_exprMgr->mkLeftAssociative(k, echildren); |