From 069949a5766abcd416c65dd0139e72b57a976e3d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 23 Nov 2018 22:30:13 -0800
Subject: [PATCH] fix model construction for semantics of itos

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

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index fb6a95790..965fdd6a5 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3519,9 +3519,8 @@ void theory_seq::add_itos_axiom(expr* e) {
     VERIFY(m_util.str.is_itos(e, n));
 
     // itos(n) = "" <=> n < 0
-    app_ref e1(m_util.str.mk_empty(m.get_sort(e)), m);
     expr_ref zero(arith_util(m).mk_int(0), m);
-    literal eq1 = mk_eq(e1, e, false);
+    literal eq1 = mk_literal(m_util.str.mk_is_empty(e));
     literal ge0 = mk_literal(m_autil.mk_ge(n, zero));
     // n >= 0 => itos(n) != ""
     // itos(n) = "" or n >= 0
@@ -3849,8 +3848,13 @@ public:
                     std::ostringstream strm;
                     arith_util arith(th.m);
                     VERIFY(arith.is_numeral(values[j++], val));
-                    if (val.is_neg()) strm << "-";
-                    strm << abs(val);
+                    
+                    if (val.is_neg()) {
+                        strm << "";
+                    }
+                    else {
+                        strm << val;
+                    }
                     zstring zs(strm.str().c_str());
                     add_buffer(sbuffer, zs);
                     break;