Add a with a procedure "in" parameter which is an element of an array…

testsuite/gnat2goto/tests/enum_in_param/enum_in.adb

@@ -0,0 +1,24 @@
+procedure Enum_In is
+   type Enum is (One, Two, Three, Four, Five, Six);
+
+   subtype More_Than_Two is Enum range Three .. Six;
+
+   type Number_Array_Type is array (1 .. 6) of Enum;
+
+   Number_Array : constant Number_Array_Type :=
+     (1 => One,
+      2 => Two,
+      3 => Three,
+      4 => Four,
+      5 => Five,
+      6 => Six);
+
+   procedure P_Enum_In (E : Enum) is
+   begin
+      if E > Two then
+         pragma Assert (E in More_Than_Two);
+      end if;
+   end P_Enum_In;
+begin
+   P_Enum_In (Number_Array (4));
+end Enum_In;

testsuite/gnat2goto/tests/enum_in_param/test.opt

@@ -0,0 +1 @@
+ALL XFAIL gnat2goto failed precondition from ireps.ads:1655

testsuite/gnat2goto/tests/enum_in_param/test.out

@@ -0,0 +1,5 @@
+[precondition_instance.1] memcpy src/dst overlap: SUCCESS
+[precondition_instance.2] memcpy source region readable: SUCCESS
+[precondition_instance.3] memcpy destination region writeable: SUCCESS
+[1] file enum_in.adb line 19 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/enum_in_param/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()