From 392d4e5782e2e896ddbda9bd04be40f7d8436256 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 21 Nov 2021 18:35:52 -0600 Subject: [PATCH] Fix const RE test for internal regexp rv kind (#7678) Fixes #7677. --- src/theory/strings/regexp_entail.cpp | 4 ++++ test/regress/CMakeLists.txt | 1 + .../regress1/strings/issue7677-test-const-rv.smt2 | 14 ++++++++++++++ 3 files changed, 19 insertions(+) create mode 100644 test/regress/regress1/strings/issue7677-test-const-rv.smt2 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) -- 2.30.2