Fix case where RE unfolding generates a trivially true lemma (#6267)

An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.

An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).

This PR ensures we are robust to these cases.

This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.

1 files changed, 13 insertions, 8 deletions

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 7737a90f7..0db536d1b 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -284,16 +284,21 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             }
             InferenceId inf =
                 polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG;
-            d_im.sendInference(iexp, noExplain, conc, inf);
-            addedLemma = true;
-            processed.push_back(assertion);
-            if (e == 0)
+            // in very rare cases, we may find out that the unfolding lemma
+            // for a membership is equivalent to true, in spite of the RE
+            // not being rewritten to true.
+            if (d_im.sendInference(iexp, noExplain, conc, inf))
             {
-              // Remember that we have unfolded a membership for x
-              // notice that we only do this here, after we have definitely
-              // added a lemma.
-              repUnfold.insert(rep);
+              addedLemma = true;
+              if (e == 0)
+              {
+                // Remember that we have unfolded a membership for x
+                // notice that we only do this here, after we have definitely
+                // added a lemma.
+                repUnfold.insert(rep);
+              }
             }
+            processed.push_back(assertion);
           }
           else
           {