mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-07-13 14:20:21 -07:00
parent b81f70f6fc
commit 8e23af33d7
1 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_seq.cpp
View file

@ -2793,19 +2793,19 @@ bool theory_seq::get_length(expr* e, rational& val) {
todo.push_back(c); todo.push_back(c);
else if (m_util.str.is_string(c, s)) else if (m_util.str.is_string(c, s))
val += rational(s.length()); val += rational(s.length());
else else {
continue; len = mk_len(c);
len = mk_len(c); if (!has_length(c)) {
if (!has_length(c)) { add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0)))); TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";);
TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";); return false;
return false; }
} else if (m_arith_value.get_value(len, val1) && !val1.is_neg())
else if (m_arith_value.get_value(len, val1) && !val1.is_neg()) val += val1;
val += val1; else {
else { TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";);
TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";); return false;
return false; }
} }
} }
CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";); CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";);