[code-simplifier] simplify seq_subset dead checks and clean profiling artifact (#9811)

This change simplifies `seq_subset` by removing redundant/dead subset
checks introduced in recent regex-subset refactoring, while preserving
behavior. It also removes an accidentally committed profiling output and
prevents recurrence.

- **`seq_subset` dead-code reduction**
  - Kept the explicit `e ⊆ a*` fast path.
- Removed the duplicate `R ⊆ R*` branch that repeated the same
star-subset recursion with a stricter depth budget.
- Clarified the remaining `a ⊆ a*` comment and cleaned trailing
whitespace.

- **Repository hygiene**
  - Deleted committed runtime artifact: `gmon.out`.
  - Added `gmon.out` to `.gitignore` to avoid future accidental commits.

Example of the simplification in `seq_subset.cpp`:

```cpp
// kept
// e ⊆ a*
if (m_re.is_epsilon(a) && m_re.is_star(b, b1))
    return true;

// kept
// 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;

// removed redundant case:
// - duplicate star-subset recursion at depth + 1
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

.gitignore

@@ -6,6 +6,7 @@ crashes/
 *.pyo
 # Ignore callgrind files
 callgrind.out.*
+gmon.out
 # .hpp files are automatically generated
 *.hpp
 .env

src/ast/rewriter/seq_subset.cpp

@@ -19,7 +19,7 @@ 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 +30,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,16 +39,12 @@ 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*
-        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))
+        // 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;
 
         // R1* ⊆ R2* if R1 ⊆ R2