From 164a73febb5fcf0eaa47ce7bf6b49832119a5573 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Apr 2020 19:23:23 -0700
Subject: [PATCH] fixing #3933 - remove unclear code normalizing itos

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 45 ++++--------------------------------------
 1 file changed, 4 insertions(+), 41 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 8751c1ae2..44bb74dea 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3924,7 +3924,9 @@ void theory_seq::add_itos_axiom(expr* e) {
     // itos(n) does not start with "0" when n > 0
     // n = 0 or at(itos(n),0) != "0"
     // alternative: n >= 0 => itos(stoi(itos(n))) = itos(n)
-    add_axiom(mk_eq(n, zero, false), ~mk_eq(m_util.str.mk_at(e,zero), m_util.str.mk_string(symbol("0")), false));
+    add_axiom(mk_eq(n, zero, false), 
+              ~mk_eq(m_util.str.mk_at(e,zero), 
+                     m_util.str.mk_string(symbol("0")), false));
     // add_axiom(~ge0, mk_preferred_eq(m_util.str.mk_itos(stoi), e));
 }
 
@@ -4869,46 +4871,7 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
         }
     }
     else if (m_util.str.is_itos(e, e1)) {
-        rational val;
-        TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
-        if (get_num_value(e1, val)) {
-            TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " -> " << val << "\n";);
-            expr_ref num(m), res(m);
-            num = m_autil.mk_numeral(val, true);
-            if (!ctx.e_internalized(num)) {
-                ctx.internalize(num, false);
-            }
-            enode* n1 = ctx.get_enode(num);
-            enode* n2 = ctx.get_enode(e1);
-            res = m_util.str.mk_string(symbol(val.to_string().c_str()));
-#if 1
-            if (val.is_neg()) {
-                result = e;
-            }
-            // TBD remove this: using roots is unsound for propagation.
-            else if (n1->get_root() == n2->get_root()) {
-                result = res;
-                deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
-            }
-            else {
-                TRACE("seq", tout << "mk equalities\n";);
-                literal l1 = mk_preferred_eq(num, e1);
-                literal l2 = mk_preferred_eq(e, res);
-                TRACE("seq", tout << "add axiom " << l1 << " " << l2 << "\n";);                
-                add_axiom(l1, ~l2);
-                add_axiom(~l1, l2);
-                result = e;
-            }
-#else
-            TRACE("seq", tout << "add axiom\n";);                
-            add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false));
-            add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
-            result = e;
-#endif
-        }
-        else {
-            result = e;
-        }
+        result = e;        
     }
     else {
         result = e;