From 1a5d663138af2025302f680a6b66a3c32d516984 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
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);