[Z3] Distinguish unknown value counts from unsat

[KellyFrog]

Slightly changed the semantic of CountSatisfyingValues as shown in source code.

Now CountSatisfyingValues returns -1 when encountering Unknown (possibly due to exceeding rlimit internal ticks).

The modified method was used 3 times in Tilelang:

• src/backend/common/op/reduce.h:142 (temporarily fallbacked to max - min + 1)
• src/transform/thread_storage_sync.cc:359

    int64_t z3_count =
        analyzer_->z3_prover.CountSatisfyingValues(iv->var, extent);
    if (z3_count > 0) {
      return static_cast<size_t>(z3_count);
    }

    // Fallback to range-based calculation if Z3 enumeration failed
    return static_cast<size_t>(bound->max_value - bound->min_value + 1);

• src/transform/thread_storage_sync.cc:475

      With<arith::ConstraintContext> ctx(analyzer_, expr);
      auto count = analyzer_->z3_prover.CountSatisfyingValues(
          iv->var, thread_extent, /*min_consecutive=*/warp_size_);
      if (count < 0) {
        // ThreadPartialSyncRewriter cannot safely lower this condition.
        current_.requires_hoist = true;

They all fallback when return code < 0, which is the expected behavior when CountSatisfyingValues gives uncertain answers.