From dde8da853ef2ebdf74a19a75a7392fa54c63fd10 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Nov 2019 13:55:55 -0800
Subject: [PATCH] fix bug introduced when fixing #2721
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_seq.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index c8b3e50f6..53deab912 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3793,10 +3793,10 @@ void theory_seq::add_itos_axiom(expr* e) {
app_ref stoi(m_util.str.mk_stoi(e), m);
add_axiom(~ge0, mk_preferred_eq(stoi, n));
- // itos(n) does not start with "0"
- // at(itos(n),0) != "0"
+ // itos(n) does not start with "0" when n > 0
+ // n = 0 or at(itos(n),0) != "0"
// alternative: n >= 0 => itos(stoi(itos(n))) = itos(n)
- add_axiom(~mk_eq(m_util.str.mk_at(e,zero), m_util.str.mk_string(symbol("0")), false));
+ add_axiom(mk_eq(n, zero, false), ~mk_eq(m_util.str.mk_at(e,zero), m_util.str.mk_string(symbol("0")), false));
// add_axiom(~ge0, mk_preferred_eq(m_util.str.mk_itos(stoi), e));
}