Count regex bisim steps during leaf traversal

[peter941221]

This picks up the seq_regex_bisim step-bound item from #9839 and leaves the other review suggestions out of scope.

Problem

seq_regex_bisim tracks a step budget through m_steps, but the old accounting only charged one step per outer worklist iteration.

That missed the internal work in collect_leaves(), which walks the derivative ITE/union tree. A small step bound could still traverse a larger derivative tree and return a definite answer instead of stopping with l_undef.

The new regression shows the gap with

re.union(re.to_re("a"), re.to_re("b"))
re.union(re.to_re("a"), re.to_re("c"))

Before this patch, the default run returns l_false, and step_bound = 1 also returned l_false. The second result means the bound did not cover the actual traversal work.

Change

collect_leaves() now increments m_steps for each visited derivative-tree node and bails out when the bound is exhausted.

The outer loop keeps the existing guard, but it no longer consumes an extra step itself. That makes the budget track the leaf traversal work that dominates this path.

Tests

I added a focused unit test in src/test/seq_regex_bisim.cpp and registered it in test-z3.

The test checks that the witness above still returns l_false with the default bound and returns l_undef after set_step_bound(1).

Validation

./test-z3 seq_regex_bisim /seq
./test-z3 smt_context /seq