From 9d3c8a6a2fa489251502b548af1fe2c3cae92ef7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 1 Jan 2022 17:59:31 -0800
Subject: [PATCH] na

---
 src/ast/rewriter/seq_axioms.cpp | 8 ++++----
 src/smt/seq_axioms.h            | 1 +
 src/smt/theory_seq.cpp          | 4 ++++
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 31057313d..bc3b6c66e 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1085,10 +1085,10 @@ namespace seq {
         sort* domain[4] = { srt, srt, srt, srt };
         auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true);
         func_decl* ra = d.get_def()->get_decl();
-        var_ref vs(m.mk_var(0, srt), m);
-        var_ref vp(m.mk_var(1, srt), m);
-        var_ref vt(m.mk_var(2, srt), m);
-        var_ref vr(m.mk_var(3, srt), m);
+        var_ref vs(m.mk_var(3, srt), m);
+        var_ref vp(m.mk_var(2, srt), m);
+        var_ref vt(m.mk_var(1, srt), m);
+        var_ref vr(m.mk_var(0, srt), m);
         var* vars[4] = { vs, vp, vt, vr };
         expr_ref test1(seq.str.mk_is_empty(vs), m);
         expr_ref branch1(seq.str.mk_is_empty(vr), m);
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index e9fc3cb53..525f6b3db 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -73,6 +73,7 @@ namespace smt {
         void add_indexof_axiom(expr* n) { m_ax.indexof_axiom(n); }
         void add_last_indexof_axiom(expr* n) { m_ax.last_indexof_axiom(n); }
         void add_replace_axiom(expr* n) { m_ax.replace_axiom(n); }
+        void add_replace_all_axiom(expr* n) { m_ax.replace_all_axiom(n); }
         void add_at_axiom(expr* n) { m_ax.at_axiom(n); }
         void add_nth_axiom(expr* n) { m_ax.nth_axiom(n); }
         void add_itos_axiom(expr* n) { m_ax.itos_axiom(n); }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 5ef415d6a..c86db1aa5 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2646,6 +2646,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_replace(n)) {
         m_ax.add_replace_axiom(n);
     }
+    else if (m_util.str.is_replace_all(n)) {
+        m_ax.add_replace_all_axiom(n);
+    }
     else if (m_util.str.is_extract(n)) {
         m_ax.add_extract_axiom(n);
     }
@@ -3190,6 +3193,7 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_to_code(n) ||
         m_util.str.is_unit(n) ||
         m_util.str.is_length(n) || 
+        /* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */
         m_util.str.is_le(n)) {
         enque_axiom(n);
     }