From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 24 May 2021 15:55:17 +0000 (-0500)
Subject: Fix instance of no rewrite in extended rewriter (#6610)
X-Git-Tag: cvc5-1.0.0~1704
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93a3d6a65db331008d590c4bb7fc0658ff1e46e0;p=cvc5.git

Fix instance of no rewrite in extended rewriter (#6610)

Fixes #6545.

An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
---

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index e73323e48..aa7e183bb 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -508,13 +508,13 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
       // must use partial substitute here, to avoid substitution into witness
       std::map<Kind, bool> rkinds;
       nn = partialSubstitute(t1, vars, subs, rkinds);
+      nn = Rewriter::rewrite(nn);
       if (nn != t1)
       {
         // If full=false, then we've duplicated a term u in the children of n.
         // For example, when ITE pulling, we have n is of the form:
         //   ite( C, f( u, t1 ), f( u, t2 ) )
         // We must show that at least one copy of u dissappears in this case.
-        nn = Rewriter::rewrite(nn);
         if (nn == t2)
         {
           new_ret = nn;
diff --git a/test/regress/regress1/strings/issue6545-extr.smt2 b/test/regress/regress1/strings/issue6545-extr.smt2
new file mode 100644
index 000000000..958f3b1ee
--- /dev/null
+++ b/test/regress/regress1/strings/issue6545-extr.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(assert
+ (str.contains ""
+  (str.replace_all ""
+   (str.substr a 1
+    (str.to_int
+     (str.substr
+      (str.substr a 0
+       (ite (= (str.len (str.substr a 2 1)) 1)
+        (ite (< (str.len a) 0)
+         (ite (= (str.len (str.substr (str.substr a 2 1) (str.len (str.substr a 1 1)) 2)) 1) 1 0)
+         (- 1))
+        0))
+      0 2)))
+   a)))
+(check-sat)