mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 16:40:52 +00:00
Code Activity

Remove redundant zero-guards before u_gcd calls in concat/intersection cases

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-11 04:26:26 +00:00
parent 4cdfceabc5
commit 35ee8f917d
1 changed files with 0 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/seq/nseq_parikh.cpp
View file

@ -137,10 +137,6 @@ namespace seq {
if (seq.re.is_concat(re, r1, r2)) { if (seq.re.is_concat(re, r1, r2)) {
unsigned s1 = compute_length_stride(r1); unsigned s1 = compute_length_stride(r1);
unsigned s2 = compute_length_stride(r2); unsigned s2 = compute_length_stride(r2);
// 0 (fixed) on either side: result is governed by the other.
if (s1 == 0 && s2 == 0) return 0;
if (s1 == 0) return s2;
if (s2 == 0) return s1;
return u_gcd(s1, s2); return u_gcd(s1, s2);
} }
@ -185,9 +181,6 @@ namespace seq {
if (seq.re.is_intersection(re, r1, r2)) { if (seq.re.is_intersection(re, r1, r2)) {
unsigned s1 = compute_length_stride(r1); unsigned s1 = compute_length_stride(r1);
unsigned s2 = compute_length_stride(r2); unsigned s2 = compute_length_stride(r2);
if (s1 == 0 && s2 == 0) return 0;
if (s1 == 0) return s2;
if (s2 == 0) return s1;
return u_gcd(s1, s2); return u_gcd(s1, s2);
} }