diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-21 18:35:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-21 16:35:52 -0800 |
| commit | 392d4e5782e2e896ddbda9bd04be40f7d8436256 (patch) | |
| tree | 06dc5c459b789c4cc8513b319010144b7b3d4857 | |
| parent | b984eae6a8608993b8ec13fa8b56ca1d67332e9a (diff) | |
Fix const RE test for internal regexp rv kind (#7678)
Fixes #7677.
| -rw-r--r-- | src/theory/strings/regexp_entail.cpp | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue7677-test-const-rv.smt2 | 14 |
3 files changed, 19 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index c9d890358..49992f14f 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -355,6 +355,10 @@ bool RegExpEntail::isConstRegExp(TNode t) return false; } } + else if (ck == REGEXP_RV) + { + return false; + } else if (ck == REGEXP_RANGE) { for (const Node& cn : cur) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7806eb308..f4e9e287b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2314,6 +2314,7 @@ set(regress_1_tests regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 regress1/strings/issue6973-dup-lemma-conc.smt2 + regress1/strings/issue7677-test-const-rv.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue7677-test-const-rv.smt2 b/test/regress/regress1/strings/issue7677-test-const-rv.smt2 new file mode 100644 index 000000000..09bd5f2b8 --- /dev/null +++ b/test/regress/regress1/strings/issue7677-test-const-rv.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun a () String) +(declare-fun b () String) +(assert + (str.in_re (str.++ a "C" b) + (re.* + (re.++ (re.union (str.to_re "A") (str.to_re "B")) + (re.* + (re.++ (re.union (str.to_re "A") (str.to_re "B")) + (re.* (str.to_re "A")) + (re.union (str.to_re "B") (str.to_re "C")))) + (re.union (str.to_re "B") (str.to_re "C")))))) +(check-sat) |