From 1a5d663138af2025302f680a6b66a3c32d516984 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 25 Apr 2020 13:25:30 -0500 Subject: [PATCH] z3str3: disallow leading zeroes in int-to-string conversion --- src/smt/theory_str.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 98e36a6a9..f44c056ff 100644 --- 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);