From fc74689c1ba500c6eefd4f0d73c04cffbb3ae820 Mon Sep 17 00:00:00 2001
From: Federico Mora <fmorarocha@gmail.com>
Date: Tue, 26 Nov 2019 17:09:52 -0800
Subject: [PATCH] int.to.str must not begin with 0 unless is 0

---
 src/smt/theory_str.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index d68641166..5142942ff 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1879,6 +1879,10 @@ namespace smt {
             expr_ref axiom1(ctx.mk_eq_atom(axiom1_lhs, axiom1_rhs), m);
             SASSERT(axiom1);
             assert_axiom(axiom1);
+
+            expr_ref zero(mk_string("0"), m);
+            expr_ref pref(u.str.mk_prefix(zero, ex), m);
+            assert_implication(pref, ctx.mk_eq_atom(ex, zero));
         }
     }