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 4e2762321b13085ccb332044df1697f57fdd5f88..5f945f465dee42da19f1d25a18b32128a4f4dc10 100644 (file)
--- 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 59ed342f2cf72caf4adf35613141300b91ac52a1..a9f2672530d005fe7c906218a63f0b45706d1900 100644 (file)
--- 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());