String smoke tests: ensure no type mismatches are seen

Type mismatches previously resulted from the expression simplifier removing casts
from one struct type to another, so e.g. (struct A)b would be simplified to b,
changing its type and leading to an equality with a type mismatch. Now that the
simplifier has been fixed this should no longer happen -- this change ensures that
none of the smoke tests generate the warning any longer.

Author: smowton

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$
 --
+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