From 35ee8f917d02839d675a97b7fd7eb5238ec181c3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 11 Mar 2026 04:26:26 +0000 Subject: [PATCH] Remove redundant zero-guards before u_gcd calls in concat/intersection cases Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/nseq_parikh.cpp | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/smt/seq/nseq_parikh.cpp b/src/smt/seq/nseq_parikh.cpp index a6d1d20e5..9ee4690b8 100644 --- a/src/smt/seq/nseq_parikh.cpp +++ b/src/smt/seq/nseq_parikh.cpp @@ -137,10 +137,6 @@ namespace seq { if (seq.re.is_concat(re, r1, r2)) { unsigned s1 = compute_length_stride(r1); 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); } @@ -185,9 +181,6 @@ namespace seq { if (seq.re.is_intersection(re, r1, r2)) { unsigned s1 = compute_length_stride(r1); 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); }