Range test: validate range_1 variable intervals against Z3-derived bounds

[Copilot]

range_1 previously validated range analysis by checking hardcoded output strings, which does not verify computed bounds semantically. This updates the test to assert per-variable interval equality between analyzer output and Z3-solved bounds.

• Range assertion model

  • Replaced string-presence checks in test_range_analysis with structured comparisons: parse each target local’s Regular [lb, ub] interval, then compare against Z3-derived (min, max) for the same constraints.
  • Keeps the same variable coverage (_20, _47, _25, _28, _39, _29, _41, _33, _34, _38, _40, _46) while making validation semantic instead of textual.

• Test utilities

  • Added parse_range_line(output, local_name) to extract concrete bounds from analysis output.
  • Added z3_interval(local_name, lower_bound, upper_bound) using z3::Optimize to compute min/max bounds under interval constraints.

• Cleanup

  • Renamed test_interprocedual_range_analysis to test_interprocedural_range_analysis for consistency/readability.

for (local_name, z3_expected) in expected_ranges {
    let analyzed = parse_range_line(&output, local_name).unwrap();
    assert_eq!(
        analyzed, z3_expected,
        "Range mismatch for local '{}': analyzed={:?}, z3={:?}",
        local_name, analyzed, z3_expected
    );
}