mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix bug introduced when fixing #2721

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-18 13:55:55 -08:00
parent 9b72b60949
commit dde8da853e
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_seq.cpp
View file

@ -3793,10 +3793,10 @@ void theory_seq::add_itos_axiom(expr* e) {
app_ref stoi(m_util.str.mk_stoi(e), m); app_ref stoi(m_util.str.mk_stoi(e), m);
add_axiom(~ge0, mk_preferred_eq(stoi, n)); add_axiom(~ge0, mk_preferred_eq(stoi, n));
// itos(n) does not start with "0" // itos(n) does not start with "0" when n > 0
// at(itos(n),0) != "0" // n = 0 or at(itos(n),0) != "0"
// alternative: n >= 0 => itos(stoi(itos(n))) = itos(n) // 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)); // add_axiom(~ge0, mk_preferred_eq(m_util.str.mk_itos(stoi), e));
} }