mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-03 02:18:58 +00:00
Code Activity

Missing case in concatenation

Browse source
This commit is contained in:
CEisenhofer 2026-04-02 20:07:51 +02:00
parent a81ce477f5
commit 9b3826ed86
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/seq/seq_nielsen.cpp
View file

@ -2898,6 +2898,7 @@ namespace seq {
expr_ref p(m), q(m);
if (seq.re.is_epsilon(left)) p = pair.m_p;
else if (seq.re.is_epsilon(pair.m_p)) p = left;
else p = seq.re.mk_concat(left, pair.m_p);
if (seq.re.is_epsilon(right)) q = pair.m_q;
else if (seq.re.is_epsilon(pair.m_q)) q = right;