diffblue · NlightNFotis · Mar 6, 2019 · Mar 6, 2019
diff --git a/testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/Use_Type_Clause.adb b/testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/Use_Type_Clause.adb
@@ -0,0 +1,8 @@
+with External_Types; use type External_Types.New_Integer;
+
+procedure Use_Type_Clause is
+   A : External_Types.New_Integer := 1;
+begin
+   A := A + 1;
+   pragma Assert (A=2);
+end Use_Type_Clause;
diff --git a/...ests/process_statement/external_types.ads → ...type_N_Use_Type_Clause/external_types.ads b/...ests/process_statement/external_types.ads → ...type_N_Use_Type_Clause/external_types.ads
diff --git a/testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/test.opt b/testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/test.opt
@@ -0,0 +1 @@
+ALL XFAIL CBMC fails with malformed symbol
diff --git a/...gnat2goto/tests/process_statement/test.py → ...ackage_use_type_N_Use_Type_Clause/test.py b/...gnat2goto/tests/process_statement/test.py → ...ackage_use_type_N_Use_Type_Clause/test.py
diff --git a/testsuite/gnat2goto/tests/process_statement/process_statement.adb b/testsuite/gnat2goto/tests/process_statement/process_statement.adb
diff --git a/testsuite/gnat2goto/tests/process_statement/test.opt b/testsuite/gnat2goto/tests/process_statement/test.opt