From 3f489edfc287678dd2f8c70eea1356b92eb1fa1c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 11 Jun 2019 18:25:07 -0700
Subject: replace lemma

---
 src/theory/strings/theory_strings.cpp | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index afdf6821f..5adae11e2 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3953,6 +3953,23 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
       // can register length term if it does not rewrite
       if (lsum == lsumb)
       {
+        if (n.getKind() == STRING_STRREPL)
+        {
+          Node len = mkLength(n[0]);
+          Node cond = nm->mkNode(GEQ, mkLength(n[1]), mkLength(n[2]));
+          Node lem = nm->mkNode(
+              ITE,
+              cond,
+              nm->mkNode(LEQ, lsum, len),
+              nm->mkNode(
+                  LEQ,
+                  lsum,
+                  nm->mkNode(
+                      PLUS,
+                      len,
+                      nm->mkNode(MINUS, mkLength(n[2]), mkLength(n[1])))));
+          d_out->lemma(lem);
+        }
         registerLength(n, LENGTH_SPLIT);
         return;
       }
-- 
cgit v1.2.3