+ // currently by the semantics of replace, if the second argument is
+ // empty, then we return the first argument.
+ // hence, we test whether the second argument must be non-empty here.
+ // if it definitely non-empty, we can use rules that successfully replace
+ // node[1]->node[2] among those below.
+ Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
+ Node zero = NodeManager::currentNM()->mkConst(CVC4::Rational(0));
+ bool is_non_empty = checkEntailArith(l1, zero, true);
+
+ if (node[0] == node[1] && is_non_empty)
+ {
+ return returnRewrite(node, node[2], "rpl-replace");
+ }