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

fix model construction for semantics of itos

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-23 22:30:13 -08:00
parent 20a28af225
commit 069949a576
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_seq.cpp
View file

@ -3519,9 +3519,8 @@ void theory_seq::add_itos_axiom(expr* e) {
VERIFY(m_util.str.is_itos(e, n));
// itos(n) = "" <=> n < 0
app_ref e1(m_util.str.mk_empty(m.get_sort(e)), m);
expr_ref zero(arith_util(m).mk_int(0), m);
literal eq1 = mk_eq(e1, e, false);
literal eq1 = mk_literal(m_util.str.mk_is_empty(e));
literal ge0 = mk_literal(m_autil.mk_ge(n, zero));
// n >= 0 => itos(n) != ""
// itos(n) = "" or n >= 0
@ -3849,8 +3848,13 @@ public:
std::ostringstream strm;
arith_util arith(th.m);
VERIFY(arith.is_numeral(values[j++], val));
if (val.is_neg()) strm << "-";
strm << abs(val);
if (val.is_neg()) {
strm << "";
}
else {
strm << val;
}
zstring zs(strm.str().c_str());
add_buffer(sbuffer, zs);
break;