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