Merge pull request #1696 from smowton/smowton/fix/identical_struct_equality

Replace unsound struct-cast simplification

Author: tautschnig

regression/strings-smoke-tests/java_append_char/test.desc

@@ -1,8 +1,9 @@
 CORE
 test_append_char.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_append_char.java line 23 .* SUCCESS
 assertion.* file test_append_char.java line 25 .* FAILURE
 --
+non equal types

regression/strings-smoke-tests/java_append_int/test.desc

@@ -1,7 +1,8 @@
 FUTURE
 test_append_int.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_append_object/test.desc

@@ -1,8 +1,10 @@
 FUTURE
 test_append_object.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
+--
 Issue: diffblue/test-gen#82

regression/strings-smoke-tests/java_append_string/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_append_string.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_append_string/test_substring.desc

@@ -1,10 +1,11 @@
 CORE
 test_append_string.class
---refine-strings --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
+--refine-strings --verbosity 10 --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.*\].* line 22.* SUCCESS$
 ^\[.*assertion.*\].* line 23.* SUCCESS$
 ^\[.*assertion.*\].* line 24.* SUCCESS$
 ^\[.*assertion.*\].* line 25.* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_case/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$
@@ -10,3 +10,4 @@ assertion.* file test_case.java line 16 .* FAILURE$
 assertion.* file test_case.java line 20 .* SUCCESS$
 assertion.* file test_case.java line 24 .* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_char_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 .*assertion.* test_char_array.java line 7 .* SUCCESS$
@@ -12,3 +12,4 @@ test_char_array.class
 .*assertion.* test_char_array.java line 29 .* FAILURE$
 ^VERIFICATION FAILED$
 --
+non equal types

regression/strings-smoke-tests/java_char_array_init/test.desc

@@ -1,8 +1,10 @@
 FUTURE
 test_init.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
+--
 cbmc/test-gen#259

regression/strings-smoke-tests/java_char_at/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_char_at.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_code_point/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_code_point.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_compare/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_compare.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_concat/test.desc

@@ -1,8 +1,9 @@
 CORE
 test_concat.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
 ^\[.*assertion.2\].* line 11.* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_contains/test.desc

@@ -1,11 +1,12 @@
 CORE
 test_contains.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
 --
 Issue: diffblue/test-gen#201

regression/strings-smoke-tests/java_contains/test_string_printable.desc

@@ -1,12 +1,13 @@
 KNOWNBUG
 test_contains.class
---refine-strings --string-max-length 100 --string-printable
+--refine-strings --verbosity 10 --string-max-length 100 --string-printable
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
 --
 This should create a huge formula and run out of memory.
 Issue: https://github.com/diffblue/test-gen/issues/745

regression/strings-smoke-tests/java_delete/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_delete.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_delete_char_at/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_delete_char_at.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_empty/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_empty.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_endswith/test.desc

@@ -1,8 +1,9 @@
 CORE
 test_endswith.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 10.* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_equal/test.desc

@@ -1,8 +1,9 @@
 CORE
 test_equal.class
---refine-strings --string-max-length 100 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* FAILURE$
 ^\[.*assertion.2\].* line 9.* SUCCESS$
 --
+non equal types

regression/strings-smoke-tests/java_equal/test_2.desc

@@ -1,7 +1,9 @@
 KNOWNBUG
 test_equal_2.class
---refine-strings --string-max-length 100 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --string-max-length 100
 ^EXIT=0$
 ^SIGNAL=0$
 --
+non equal types
+--
 https://github.com/diffblue/test-gen/issues/856

regression/strings-smoke-tests/java_float/test.desc

@@ -1,7 +1,8 @@
 FUTURE
 test_float.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_format/test.desc

@@ -1,9 +1,10 @@
 CORE
 test.class
---refine-strings --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
 --
+non equal types
 ^ignoring

regression/strings-smoke-tests/java_format2/test.desc

@@ -1,9 +1,10 @@
 CORE
 test.class
---refine-strings --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
 --
+non equal types
 ^warning

regression/strings-smoke-tests/java_format3/test.desc

@@ -1,9 +1,10 @@
 CORE
 test.class
---refine-strings --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* FAILURE$
 --
+non equal types
 ^warning

regression/strings-smoke-tests/java_format4/test.desc

@@ -1,8 +1,9 @@
 KNOWNBUG
 test.class
---refine-strings --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 13.* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_format5/test.desc

@@ -1,8 +1,9 @@
 THOROUGH
 test.class
---refine-strings --string-max-length 20
+--refine-strings --verbosity 10 --string-max-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_hash_code/test.desc

@@ -1,8 +1,9 @@
 CORE
 test_hash_code.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_if/test.desc

@@ -1,9 +1,10 @@
 CORE
 test.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 11.* SUCCESS$
 ^\[.*assertion.2\].* line 13.* FAILURE$
 --
-$ignoring\s*char\s*array
+non equal types
+ignoring\s*char\s*array

regression/strings-smoke-tests/java_index_of/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_index_of.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_index_of2/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_index_of2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+non equal types

regression/strings-smoke-tests/java_index_of_char/test.desc

@@ -1,8 +1,10 @@
 CORE
 test_index_of_char.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
+--
 Issue: cbmc/test-gen#77

regression/strings-smoke-tests/java_insert_char/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_insert_char.class
---refine-strings  --string-max-length 1000
+--refine-strings --verbosity 10  --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_insert_char_array/test.desc

@@ -1,8 +1,9 @@
 CORE
 test_insert_char_array.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_insert_char_array.java line 20 .* SUCCESS$
 assertion.* file test_insert_char_array.java line 22 .* FAILURE$
 --
+non equal types

regression/strings-smoke-tests/java_insert_int/test.desc

@@ -1,7 +1,8 @@
 FUTURE
 test_insert_int.class
---refine-strings  --string-max-length 1000
+--refine-strings --verbosity 10  --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types

regression/strings-smoke-tests/java_insert_multiple/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_insert_multiple.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types