From 8881084449d190b45d12f94f4a64d8e2a6104ad0 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 28 Feb 2020 18:14:25 -0500
Subject: [PATCH] z3str3: reduce int-to-string in bitvector model construction

---
 src/smt/theory_str_mc.cpp | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index 9c9c3efa1..2fe97c32c 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -712,6 +712,28 @@ namespace smt {
                 eqc_chars.push_back(base_chars.get(pos_value.get_unsigned()));
             }
             return true;
+	} else if (u.str.is_itos(term, arg0)) {
+	    expr_ref i(arg0, m);
+	    arith_value v(m);
+	    v.init(&get_context());
+	    rational iValue;
+	    bool iValue_exists = v.get_value(i, iValue);
+	    if (!iValue_exists) {
+	        NOT_IMPLEMENTED_YET(); // TODO force assignment in arith solver
+	    }
+	    TRACE("str_fl", tout << "reduce int.to.str: n=" << iValue << std::endl;);
+	    if (iValue.is_neg()) {
+  	        // return the empty string
+	        eqc_chars.reset();
+	    } else {
+	        // convert iValue to a constant
+	        zstring iValue_str = zstring(iValue.to_string().c_str());
+		for (unsigned idx = 0; idx < iValue_str.length(); ++idx) {
+	            expr_ref chTerm(bitvector_character_constants.get(iValue_str[idx]), sub_m);
+		    eqc_chars.push_back(chTerm);
+		}
+            }
+	    return true;
         } else {
             TRACE("str_fl", tout << "string term " << mk_pp(term, m) << " handled as uninterpreted function" << std::endl;);
             if (!uninterpreted_to_char_subterm_map.contains(term)) {