From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Nov 2021 00:35:52 +0000 (-0600)
Subject: Fix const RE test for internal regexp rv kind (#7678)
X-Git-Tag: cvc5-1.0.0~791
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=392d4e5782e2e896ddbda9bd04be40f7d8436256;p=cvc5.git

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 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)