Fix const RE test for internal regexp rv kind (#7678)

Fixes #7677.

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index c9d890358d4aa58bdca2ae77e381b07d48c60d83..49992f14f8ae0f0cae01acfb1e31b86d82993571 100644 (file)
--- 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 7806eb308d9e07ba95cc4c24e369a1d74b97dd1c..f4e9e287bf883dc5d4f4d0fe54171cacb74da20d 100644 (file)
--- 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 (file)
index 0000000..09bd5f2
--- /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)