diffblue · martin-cs · Jan 28, 2020 · Jan 14, 2020
diff --git a/testsuite/gnat2goto/tests/deferred_constant_use/test.opt b/testsuite/gnat2goto/tests/deferred_constant_use/test.opt
diff --git a/testsuite/gnat2goto/tests/deferred_constant_use/test.out b/testsuite/gnat2goto/tests/deferred_constant_use/test.out
@@ -1,4 +1,2 @@
-[assertion.1] Range Check: SUCCESS
-VERIFICATION SUCCESSFUL
-
+[inc.assertion.1] line 4 Ada Check assertion: SUCCESS
 VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt
diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out
@@ -1 +1,2 @@
+[range_constraint.assertion.1] line 15 assertion Value = CALIBRATION_FAIL: SUCCESS
 VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/packages/test.opt b/testsuite/gnat2goto/tests/packages/test.opt
diff --git a/testsuite/gnat2goto/tests/packages/test.out b/testsuite/gnat2goto/tests/packages/test.out
@@ -0,0 +1,3 @@
+[packages.assertion.1] line 6 assertion Test.Double (1) = 2: SUCCESS
+[double.assertion.1] line 6 Ada Check assertion: SUCCESS
+VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt b/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt
@@ -1 +1 @@
-ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects.
+ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects.
diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.out b/testsuite/gnat2goto/tests/size_integer_and_objects/test.out
Original file line number	Diff line number	Diff line change
		@@ -1 +1,2 @@
		[range_constraint.assertion.1] line 15 assertion Value = CALIBRATION_FAIL: SUCCESS
		VERIFICATION SUCCESSFUL
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects.
		ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects.