simplify: remove dead code in seq_subset and delete gmon.out

- seq_subset.cpp: Remove redundant 'e ⊆ a*' check (lines 46-48).
  When a=epsilon and b=b1*, get_info(b1*).nullable is always l_true,
  so the earlier epsilon+nullable check already handles this case.

- seq_subset.cpp: Remove redundant 'R ⊆ R*' check (lines 50-52).
  The preceding 'a ⊆ a*' check uses the same is_star condition but
  calls is_subset_rec with the same depth (more budget), making the
  depth+1 variant unreachable in any useful scenario.

- seq_subset.cpp: Remove trailing whitespace (lines 22, 33).

- Remove accidentally committed gmon.out profiling output file.

- .gitignore: Add gmon.out to prevent future accidental commits.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

.gitignore

@@ -124,3 +124,5 @@ bazel-*
 .deeptest/
 tptp_test/
 tptp_benchmarks/
+# Profiling output files
+gmon.out

src/ast/rewriter/seq_subset.cpp

@@ -19,7 +19,6 @@ Author:
 
 bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const {
     while (true) {
-        
         if (a == b)
             return true;
         if (m_re.is_empty(a))
@@ -30,7 +29,7 @@ bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const {
             return true;
 
         if (depth >= m_max_depth)
-            return false;        
+            return false;
 
         expr* a1 = nullptr, * a2 = nullptr, * b1 = nullptr, * b2 = nullptr;
         unsigned la, ua, lb, ub;
@@ -39,18 +38,10 @@ bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const {
         if (m_re.is_dot_plus(b) && m_re.get_info(a).nullable == l_false)
             return true;
 
-        // a ⊆ a*
+        // a ⊆ a*: if b = b1* and a ⊆ b1, then a ⊆ b1*
         if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth))
             return true;
 
-        // e ⊆ a*
-        if (m_re.is_epsilon(a) && m_re.is_star(b, b1))
-            return true;
-
-        // R ⊆ R*
-        if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth + 1))
-            return true;
-
         // R1* ⊆ R2* if R1 ⊆ R2
         if (m_re.is_star(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
             return true;