Add missing null terminators for regexp (#8027)

Led to some LFSC proof checking failures on strings benchmarks.

diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp
index 03ce637e47d29f117143484df2137571bb565618..500b45a81042ddf1e02b08adda4315c1754cdcde 100644 (file)
--- a/src/expr/nary_term_util.cpp
+++ b/src/expr/nary_term_util.cpp
@@ -132,6 +132,14 @@ Node getNullTerminator(Kind k, TypeNode tn)
       // the language containing only the empty string
       nullTerm = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
       break;
+    case REGEXP_UNION:
+      // empty language
+      nullTerm = nm->mkNode(REGEXP_NONE);
+      break;
+    case REGEXP_INTER:
+      // universal language
+      nullTerm = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR));
+      break;
     case BITVECTOR_AND:
       nullTerm = theory::bv::utils::mkOnes(tn.getBitVectorSize());
       break;

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 148c5d9e78a71aad31da1751e755881e5bc12822..8d1273dd258a4b388c9b43316eb6781124729c53 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -450,6 +450,8 @@ Node LfscNodeConverter::postConvert(Node n)
         ret = nm->mkNode(ck, children[i], ret);
       }
     }
+    Trace("lfsc-term-process-debug")
+        << "...return n-ary conv " << ret << std::endl;
     return ret;
   }
   return n;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 83cc6f1c8e0be52919c6d79eaaa5ff0c8f250ec2..aded275b6582e563017c91b02d1f2993d0cedf3b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2326,6 +2326,7 @@ set(regress_1_tests
   regress1/strings/idof-neg-index.smt2
   regress1/strings/idof-triv.smt2
   regress1/strings/ilc-l-nt.smt2
+  regress1/strings/instance2984-null-term.smt2
   regress1/strings/instance3303-delta.smt2
   regress1/strings/instance7075-delta.smt2
   regress1/strings/issue1105.smt2

diff --git a/test/regress/regress1/strings/instance2984-null-term.smt2 b/test/regress/regress1/strings/instance2984-null-term.smt2
new file mode 100644 (file)
index 0000000..da93890
--- /dev/null
+++ b/test/regress/regress1/strings/instance2984-null-term.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const X String)
+(assert (not (str.in_re X (re.union (str.to_re "") (re.comp (str.to_re "")) (re.* (str.to_re ""))))))
+(check-sat)