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

block unsound itos solutions. #2721

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

5
src/smt/theory_seq.cpp
View file

@ -3793,6 +3793,11 @@ 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"
// 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(~ge0, mk_preferred_eq(m_util.str.mk_itos(stoi), e));
}