From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Mar 2022 23:36:37 +0000 (-0500)
Subject: Change null terminator for regular expression intersection (#8362)
X-Git-Tag: cvc5-1.0.0~205
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8746066a6cbcf6c88d9b6da7a43d32ed3451850f;p=cvc5.git

Change null terminator for regular expression intersection (#8362)
---

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index 4e2762321..5f945f465 100644
--- a/proofs/lfsc/signatures/strings_rules.plf
+++ b/proofs/lfsc/signatures/strings_rules.plf
@@ -122,7 +122,7 @@
                               (holds s))))))
 
 (declare re_inter (! x term (! s term (! t term (! p1 (holds (str.in_re x s)) (! p2 (holds (str.in_re x t)) 
-  (holds (str.in_re x (re.inter s (re.inter t (re.* re.allchar)))))))))))
+  (holds (str.in_re x (re.inter s (re.inter t re.all))))))))))
 
 (declare string_reduction (! r term (! t term (! s sort (! u (^ (sc_string_reduction t s) r)
   (holds r))))))))
diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp
index 59ed342f2..a9f267253 100644
--- a/src/expr/nary_term_util.cpp
+++ b/src/expr/nary_term_util.cpp
@@ -138,7 +138,7 @@ Node getNullTerminator(Kind k, TypeNode tn)
       break;
     case REGEXP_INTER:
       // universal language
-      nullTerm = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR));
+      nullTerm = nm->mkNode(REGEXP_ALL);
       break;
     case BITVECTOR_AND:
       nullTerm = theory::bv::utils::mkOnes(tn.getBitVectorSize());