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 e73323e482c931b9503479e07ed012d0609539e5..aa7e183bb30ee4822acf8f4f89fe3a00efab7c4d 100644 (file)
--- 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 (file)
index 0000000..958f3b1
--- /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)