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 #5047

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-26 03:37:14 -08:00
parent ea1089e980
commit 5c47f244e9
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -496,8 +496,10 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
} }
TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";); TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false); literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
if (ctx.get_assignment(a) == l_false)
return false;
literal b = mk_seq_eq(seq, e); literal b = mk_seq_eq(seq, e);
if (ctx.get_assignment(a) == l_false || ctx.get_assignment(b) == l_true) if (ctx.get_assignment(b) == l_true)
return false; return false;
add_axiom(~a, b); add_axiom(~a, b);
if (!ctx.at_base_level()) { if (!ctx.at_base_level()) {