mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

int.to.str must not begin with 0 unless is 0

Browse source
This commit is contained in:
Federico Mora 2019-11-26 17:09:52 -08:00 • committed by Nikolaj Bjorner
parent 0b893afee4
commit fc74689c1b
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str.cpp
View file

@ -1879,6 +1879,10 @@ namespace smt {
expr_ref axiom1(ctx.mk_eq_atom(axiom1_lhs, axiom1_rhs), m);
SASSERT(axiom1);
assert_axiom(axiom1);
expr_ref zero(mk_string("0"), m);
expr_ref pref(u.str.mk_prefix(zero, ex), m);
assert_implication(pref, ctx.mk_eq_atom(ex, zero));
}
}