Range checks for subtypes not supported correctly.

[NlightNFotis]

This has been a problem that I discovered while working on supporting subtypes within enumeration symbols.

For example, this code is failing:

procedure Range_Second is
  type Indicator_Type is (
    CALIBRATION_MODE,
    MEASUREMENT_MODE,
    CALIBRATION_PASS,
    CALIBRATION_FAIL,
    MEASUREMENT_NOT_PROVEN,
    MEASUREMENT_PRESENT);

  subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;

  procedure Testable (Result : Result_Indicator_Type) is
  begin
    null;
  end Testable;

begin
  Testable (CALIBRATION_PASS);
  Testable (MEASUREMENT_PRESENT);
end Range_Second;

But the problem is not necessarily on the symbols signifying the range, as the same program with integer ranges is also failing the range checks.

procedure Range_Second is
  type An_Int is range 1..1000;
  subtype Another_Int is An_Int range 5..100;

  procedure Testable (Result : Another_Int) is
  begin
    null;
  end Testable;

begin
  Testable (50);
  Testable (200);
end Range_Second;

Failing the range checks in this case means that CBMC returns VERIFICATION SUCCESSFUL when otherwise it should have assertion failures.