diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 41701f469..4f81e859d 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1881,12 +1881,15 @@ namespace smt {
             assert_axiom(axiom1);
         }
 
-        // axiom 2: (str.from-int N) should not result in a string with leading zeros.
+        // axiom 2: The only (str.from-int N) that starts with a "0" is "0".
         expr_ref zero(mk_string("0"), m);
-        expr_ref pref(u.str.mk_prefix(zero, ex), m);
-        // The result does not start with a "0" (~p) xor the result is "0" (q)
-        // ~p xor q == (p or q) and (~p or ~q)
-        assert_axiom(m.mk_and(m.mk_or(pref, ctx.mk_eq_atom(ex, zero)), m.mk_or(mk_not(m, pref), mk_not(m, ctx.mk_eq_atom(ex, zero)))));
+        // let (the result starts with a "0") be p
+        expr_ref p(u.str.mk_prefix(zero, ex), m);
+        // let (the result is "0") be q  
+        expr_ref q(ctx.mk_eq_atom(ex, zero), m);
+        // encoding: the result does NOT start with a "0" (~p) xor the result is "0" (q)
+        // ~p xor q == (~p or q) and (p or ~q)
+        assert_axiom(m.mk_and(m.mk_or(mk_not(m, p), q), m.mk_or(p, mk_not(m, q))));
     }
 
     expr * theory_str::mk_RegexIn(expr * str, expr * regexp) {