mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-25 05:13:32 +00:00
Code Activity

Quick fix for some unsound cases

Browse source
This commit is contained in:
CEisenhofer 2026-04-04 18:36:25 +02:00
parent a58a9114d2
commit 8298ba6011
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_nseq.cpp
View file

@ -428,8 +428,7 @@ namespace smt {
}
void theory_nseq::ensure_length_var(expr* e) {
if (!e || !m_seq.is_seq(e))
return;
SASSERT(e && m_seq.is_seq(e));
expr_ref len(m_seq.str.mk_length(e), m);
if (!ctx.e_internalized(len))
ctx.internalize(len, false);