Merge pull request #4101 from mtrberzi/int-to-str-leading-zeroes

z3str3: disallow leading zeroes in int-to-string conversion
Z3Prover · Apr 29, 2020 · 0fb6a7c · 0fb6a7c
2 parents 4d54b41 + 1a5d663
commit 0fb6a7c
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
@@ -8933,11 +8933,19 @@ namespace smt {
         if (Sval_expr_exists) {
             zstring Sval;
             u.str.is_string(Sval_expr, Sval);
-            TRACE("str", tout << "string theory assigns \"" << mk_pp(a, m) << " = " << Sval << "\n";);
+            TRACE("str", tout << "string theory assigns " << mk_pp(a, m) << " = \"" << Sval << "\"\n";);
             // empty string --> integer value < 0
             if (Sval.empty()) {
                 // ignore this. we should already assert the axiom for what happens when the string is ""
             } else {
+                // check for leading zeroes. if the first character is '0', the entire string must be "0"
+                char firstChar = (int)Sval[0];
+                if (firstChar == '0' && !(Sval == zstring("0"))) {
+                    TRACE("str", tout << "str.to-int argument " << Sval << " contains leading zeroes" << std::endl;);
+                    expr_ref axiom(m.mk_not(ctx.mk_eq_atom(a, mk_string(Sval))), m);
+                    assert_axiom(axiom);
+                    return true;
+                }
                 // nonempty string --> convert to correct integer value, or disallow it
                 rational convertedRepresentation(0);
                 rational ten(10);