diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | src/theory/strings/kinds | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue5428-re-diff-assoc.smt2 | 4 |
4 files changed, 7 insertions, 2 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); diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 78c6ab1f1..020cedb30 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -90,7 +90,7 @@ operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" operator REGEXP_UNION 2: "regexp union" operator REGEXP_INTER 2: "regexp intersection" -operator REGEXP_DIFF 2: "regexp difference" +operator REGEXP_DIFF 2 "regexp difference" operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ac62452e5..ac6d91e7c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1010,6 +1010,7 @@ set(regress_0_tests regress0/strings/issue4820.smt2 regress0/strings/issue4915.smt2 regress0/strings/issue5090.smt2 + regress0/strings/issue5428-re-diff-assoc.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue5428-re-diff-assoc.smt2 b/test/regress/regress0/strings/issue5428-re-diff-assoc.smt2 new file mode 100644 index 000000000..64455f2c3 --- /dev/null +++ b/test/regress/regress0/strings/issue5428-re-diff-assoc.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_S) +(set-info :status unsat) +(assert (str.in_re "" (re.diff (re.* re.allchar) re.allchar (re.* re.allchar)))) +(check-sat) |