Unsigned integer constants sign-extended incorrectly in `const_value_ty`, causing wrong CHC terms and potential panic

[coord-e]

Bug

In src/analyze/basic_block.rs, the const_value_ty function uses ScalarInt::to_int for both signed and unsigned integer types:

// lines 383–391
(
    mir_ty::TyKind::Int(_) | mir_ty::TyKind::Uint(_),
    ConstValue::Scalar(Scalar::Int(val)),
) => {
    let val = val.to_int(val.size());   // ← sign-extends for both Int and Uint
    PlaceType::with_ty_and_term(
        rty::Type::int(),
        chc::Term::int(val.try_into().unwrap()),
    )
}

ScalarInt::to_int sign-extends the raw bit pattern from the scalar's size. For Uint(_) types this is wrong in two ways:

1. Semantically incorrect CHC terms for large unsigned values

Any u64 constant whose high bit is set (i.e., value ≥ 2⁶³ ≈ 9.2 × 10¹⁸) will be sign-extended to a negative i128 and then stored as a negative i64 in the CHC solver. For example:

const X: u64 = 10_000_000_000_000_000_000_u64; // 10^19, a valid u64

to_int(8) treats the bit pattern as a signed 64-bit integer, yielding −8_446_744_073_709_551_616. The CHC solver then reasons about X == −8_446_744_073_709_551_616, which is wrong. A refinement predicate like

#[thrust::ensures(|result| result == 10_000_000_000_000_000_000_u64)]
fn get_large() -> u64 { 10_000_000_000_000_000_000_u64 }

would fail to verify even though it is clearly correct.

2. Panic on u128/i128 constants that exceed i64::MAX

to_int(16) returns an i128. The subsequent val.try_into().unwrap() converts to i64 and panics if the value is outside [i64::MIN, i64::MAX]. For example:

const Y: u128 = 1_000_000_000_000_000_000_000_u128; // fits in u128, exceeds i64::MAX

or

const Z: i128 = i128::MAX;

Analyzing either of these causes an unwrap panic with no useful error message.

Expected behaviour

• Uint(_) constants should use to_uint (returns u128) so the value is treated as non-negative.
• The subsequent narrowing to i64 should handle values that don't fit (either by using a wider CHC integer representation or by emitting a graceful "unsupported" error rather than panicking).

Note that const_bytes_ty already handles the signed/unsigned distinction correctly for in-memory byte representations (it only covers TyKind::Int(_) with explicit byte-length matching and does not handle Uint(_) at all, falling through to unimplemented!). The const_value_ty path is therefore both inconsistent with const_bytes_ty and incorrect.

Suggested fix

(
    mir_ty::TyKind::Int(_),
    ConstValue::Scalar(Scalar::Int(val)),
) => {
    let val: i64 = val.to_int(val.size()).try_into().expect("int constant out of i64 range");
    PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(val))
}
(
    mir_ty::TyKind::Uint(_),
    ConstValue::Scalar(Scalar::Int(val)),
) => {
    let val: i64 = val.to_uint(val.size()).try_into().expect("uint constant out of i64 range");
    PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(val))
}

(The expect messages still panic for very large integers, but at least they surface a clear diagnostic. A proper fix would need to decide how to represent values that don't fit in i64.)