`PRUSTI_CHECK_OVERFLOWS=false` produces an internal error for a called pure unsigned subtraction

[lynae99]

Prusti 0.2.2 reports a normal overflow diagnostic by default, but reports an internal error when overflow checking is disabled.

Reproducer

Save the following as PureResultRangeCheckOverflows.rs:

use prusti_contracts::*;

#[pure]
fn decrease(value: usize) -> usize {
    value - 1
}

fn main() {
    decrease(0);
}

Reproduction commands

PRUSTI=/path/to/prusti-rustc
PRUSTI_HOME=/path/to/prusti
DEFAULT_OUT=$(mktemp -d)
TARGET_OUT=$(mktemp -d)

RUSTUP_TOOLCHAIN=nightly-2023-09-15 \
  "$PRUSTI" PureResultRangeCheckOverflows.rs --crate-name pure_result_range \
  --edition=2021 -L "$PRUSTI_HOME" -L "$PRUSTI_HOME/deps" \
  --out-dir "$DEFAULT_OUT"

PRUSTI_CHECK_OVERFLOWS=false RUSTUP_TOOLCHAIN=nightly-2023-09-15 \
  "$PRUSTI" PureResultRangeCheckOverflows.rs --crate-name pure_result_range \
  --edition=2021 -L "$PRUSTI_HOME" -L "$PRUSTI_HOME/deps" \
  --out-dir "$TARGET_OUT"

Actual result

The default configuration reports:

assertion might fail with "attempt to subtract with overflow"

With PRUSTI_CHECK_OVERFLOWS=false, Prusti reports:

[Prusti: internal error] Prusti encountered an unexpected internal error
Details: ... Assertion 0 <= result might not hold ...
PureFunctionPostconditionValueRangeOfResult

The result was reproduced in three independent runs.

Expected result

Disabling overflow checking should not produce an internal error. Prusti should
finish normally or report a regular diagnostic.

Version

Prusti 0.2.2, commit 0d4a8d4
rustc 1.74.0-nightly