--- /dev/null
+-- { dg-do compile }
+-- { dg-options "-O -gnatVT -fdump-tree-optimized" }
+
+-- Check that we perform the expected validity checks for
+-- hardbool-annotated types, even when checking of tests is disabled.
+
+package body Hardbool is
+ function T return Boolean is (Boolean (X) and then Boolean (Y));
+
+ procedure P1 is
+ begin
+ X := HBool1 (not Y);
+ end P1;
+
+ procedure P2 is
+ begin
+ X := HBool1 (if Y then HBool2'(False) else HBool2'(True));
+ end P2;
+
+ procedure P3 is
+ begin
+ X := (if Y then HBool1'(False) else HBool1'(True));
+ end P3;
+
+ procedure Q1 is
+ begin
+ Y := HBool2 (not X);
+ end Q1;
+
+ procedure Q2 is
+ begin
+ Y := HBool2 (if X then HBool1'(False) else HBool1'(True));
+ end Q2;
+
+ procedure Q3 is
+ begin
+ Y := (if X then HBool2'(False) else HBool2'(True));
+ end Q3;
+
+end Hardbool;
+
+-- One for each type's _rep_to_pos function.
+-- { dg-final { scan-tree-dump-times "gnat_rcheck_CE_Invalid_Data ..hardbool.ads" 2 "optimized" } }
+
+-- One check for each variable used in T, one use in each P* and in each Q*.
+-- { dg-final { scan-tree-dump-times "gnat_rcheck_CE_Invalid_Data ..hardbool.adb" 8 "optimized" } }
--- /dev/null
+package Hardbool is
+ type HBool1 is new Boolean;
+ for HBool1'Size use 8;
+ for HBool1 use (16#5a#, 16#a5#);
+ pragma Machine_Attribute (HBool1, "hardbool");
+
+ type HBool2 is new Boolean;
+ for HBool2 use (16#0ff0#, 16#f00f#);
+ for HBool2'Size use 16;
+ pragma Machine_Attribute (HBool2, "hardbool");
+
+ X : HBool1 := False;
+ Y : HBool2 := True;
+
+ function T return Boolean;
+ procedure P1;
+ procedure P2;
+ procedure P3;
+ procedure Q1;
+ procedure Q2;
+ procedure Q3;
+end Hardbool;