diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 20:02:20 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-12 20:02:20 -0600 |
| commit | 151a4bb262713a94c488f2e4e8c1f5d498098253 (patch) | |
| tree | 3eccc7180efe0a5b908ddaf9c6e0e0528a80ebe2 /src/api | |
| parent | cf7c2ce97615990388bb6c37b151c0e2b2fe8f9a (diff) | |
Make regular expression difference left associative (#5430)
Fixes #5428.
Diffstat (limited to 'src/api')
| -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 566bcc3c7..24902b888 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3248,7 +3248,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 == HO_APPLY) + || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF) { // left-associative, but CVC4 internally only supports 2 args res = d_exprMgr->mkLeftAssociative(k, echildren); |