diff --git a/regression/strings-smoke-tests/java_append_char/test.desc b/regression/strings-smoke-tests/java_append_char/test.desc
index 7ad217f7fa3..2a9b5555478 100644
--- a/regression/strings-smoke-tests/java_append_char/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc
index 17f38286a5b..71e874d2486 100644
--- a/regression/strings-smoke-tests/java_append_int/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc
index 62c1f56eea2..c905a3990f6 100644
--- a/regression/strings-smoke-tests/java_append_object/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc
index 39c04f7031d..9b6882b5f3f 100644
--- a/regression/strings-smoke-tests/java_append_string/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_append_string/test_substring.desc b/regression/strings-smoke-tests/java_append_string/test_substring.desc
index d62a4a8be0a..de4c8675ad1 100644
--- a/regression/strings-smoke-tests/java_append_string/test_substring.desc
+++ b/regression/strings-smoke-tests/java_append_string/test_substring.desc
@@ -1,6 +1,6 @@
 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$
@@ -8,3 +8,4 @@ test_append_string.class
 ^\[.*assertion.*\].* line 24.* SUCCESS$
 ^\[.*assertion.*\].* line 25.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc
index 2889787e47a..bf6722dd2f8 100644
--- a/regression/strings-smoke-tests/java_case/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc
index c5d89dd2810..3b1bf17532a 100644
--- a/regression/strings-smoke-tests/java_char_array/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_char_array_init/test.desc b/regression/strings-smoke-tests/java_char_array_init/test.desc
index 1202bb035b6..c5e050b4850 100644
--- a/regression/strings-smoke-tests/java_char_array_init/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_char_at/test.desc b/regression/strings-smoke-tests/java_char_at/test.desc
index 2be2ab204ca..5279f32726e 100644
--- a/regression/strings-smoke-tests/java_char_at/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_code_point/test.desc b/regression/strings-smoke-tests/java_code_point/test.desc
index aa7799f5170..2c3def77c28 100644
--- a/regression/strings-smoke-tests/java_code_point/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_compare/test.desc b/regression/strings-smoke-tests/java_compare/test.desc
index a7d8151b55b..8f967c8dffb 100644
--- a/regression/strings-smoke-tests/java_compare/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_concat/test.desc b/regression/strings-smoke-tests/java_concat/test.desc
index 6063f361aa5..2672b7502d2 100644
--- a/regression/strings-smoke-tests/java_concat/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_contains/test.desc b/regression/strings-smoke-tests/java_contains/test.desc
index 158cf338c0a..a0b0afc6933 100644
--- a/regression/strings-smoke-tests/java_contains/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_contains/test_string_printable.desc b/regression/strings-smoke-tests/java_contains/test_string_printable.desc
index ccd29948c26..2c0d8942b68 100644
--- a/regression/strings-smoke-tests/java_contains/test_string_printable.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_delete/test.desc b/regression/strings-smoke-tests/java_delete/test.desc
index dd957dd16bd..7fb479f198b 100644
--- a/regression/strings-smoke-tests/java_delete/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_delete_char_at/test.desc b/regression/strings-smoke-tests/java_delete_char_at/test.desc
index cfd8b4778d1..91710ffcf63 100644
--- a/regression/strings-smoke-tests/java_delete_char_at/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_empty/test.desc b/regression/strings-smoke-tests/java_empty/test.desc
index e82479e301b..c1dae21b4d5 100644
--- a/regression/strings-smoke-tests/java_empty/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_endswith/test.desc b/regression/strings-smoke-tests/java_endswith/test.desc
index 002bd3015da..2dec4153ff7 100644
--- a/regression/strings-smoke-tests/java_endswith/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_equal/test.desc b/regression/strings-smoke-tests/java_equal/test.desc
index 964c3b72bae..946129f44a6 100644
--- a/regression/strings-smoke-tests/java_equal/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_equal/test_2.desc b/regression/strings-smoke-tests/java_equal/test_2.desc
index bfa989a3695..ab7cb11a7de 100644
--- a/regression/strings-smoke-tests/java_equal/test_2.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_float/test.desc b/regression/strings-smoke-tests/java_float/test.desc
index 5f225af821a..e9df3330ee1 100644
--- a/regression/strings-smoke-tests/java_float/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_format/test.desc b/regression/strings-smoke-tests/java_format/test.desc
index 8999b5b27ec..e688c95b140 100644
--- a/regression/strings-smoke-tests/java_format/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_format2/test.desc b/regression/strings-smoke-tests/java_format2/test.desc
index f34840a743c..0ea5e37ca19 100644
--- a/regression/strings-smoke-tests/java_format2/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_format3/test.desc b/regression/strings-smoke-tests/java_format3/test.desc
index 597b65ce183..5aeac5fb776 100644
--- a/regression/strings-smoke-tests/java_format3/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_format4/test.desc b/regression/strings-smoke-tests/java_format4/test.desc
index 120bf0cf11f..51f9f2b1d29 100644
--- a/regression/strings-smoke-tests/java_format4/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_format5/test.desc b/regression/strings-smoke-tests/java_format5/test.desc
index 1a77e4be0a5..4e09fa65ada 100644
--- a/regression/strings-smoke-tests/java_format5/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_hash_code/test.desc b/regression/strings-smoke-tests/java_hash_code/test.desc
index c00e466b8c4..54d6734c0ba 100644
--- a/regression/strings-smoke-tests/java_hash_code/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_if/test.desc b/regression/strings-smoke-tests/java_if/test.desc
index 1be275e233e..a652d884b11 100644
--- a/regression/strings-smoke-tests/java_if/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc
index 3fdfa1ffc5d..e5b6c994424 100644
--- a/regression/strings-smoke-tests/java_index_of/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_index_of2/test.desc b/regression/strings-smoke-tests/java_index_of2/test.desc
index 2c9d464054c..a3744c3a776 100644
--- a/regression/strings-smoke-tests/java_index_of2/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_index_of_char/test.desc b/regression/strings-smoke-tests/java_index_of_char/test.desc
index 59d3310fa48..c457e8cd7d0 100644
--- a/regression/strings-smoke-tests/java_index_of_char/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_insert_char/test.desc b/regression/strings-smoke-tests/java_insert_char/test.desc
index 88200524d70..3281b3d629b 100644
--- a/regression/strings-smoke-tests/java_insert_char/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc
index 472ebd69890..a0614d7f360 100644
--- a/regression/strings-smoke-tests/java_insert_char_array/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_insert_int/test.desc b/regression/strings-smoke-tests/java_insert_int/test.desc
index 488e2bc8766..66c81170630 100644
--- a/regression/strings-smoke-tests/java_insert_int/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_insert_multiple/test.desc b/regression/strings-smoke-tests/java_insert_multiple/test.desc
index d3236ab78ee..5b77efb0d46 100644
--- a/regression/strings-smoke-tests/java_insert_multiple/test.desc
+++ b/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
diff --git a/regression/strings-smoke-tests/java_insert_string/test.desc b/regression/strings-smoke-tests/java_insert_string/test.desc
index 2b91905e17e..93596bf62ac 100644
--- a/regression/strings-smoke-tests/java_insert_string/test.desc
+++ b/regression/strings-smoke-tests/java_insert_string/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_insert_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
diff --git a/regression/strings-smoke-tests/java_int_to_string/test1.desc b/regression/strings-smoke-tests/java_int_to_string/test1.desc
index 318ec0fb224..fd14afd9e7f 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test1.desc
@@ -1,8 +1,9 @@
 CORE
 Test1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string/test2.desc b/regression/strings-smoke-tests/java_int_to_string/test2.desc
index 186a25d2d8b..08bb206db54 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test2.desc
@@ -1,8 +1,9 @@
 CORE
 Test2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
index 00047bad217..c2917e25045 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
@@ -1,11 +1,12 @@
 KNOWNBUG
 Test2.class
---refine-strings
+--refine-strings --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
 --
 When string-max-length is not set, the solver can run out of memory in
-an unpredictable way.
\ No newline at end of file
+an unpredictable way.
diff --git a/regression/strings-smoke-tests/java_int_to_string/test3.desc b/regression/strings-smoke-tests/java_int_to_string/test3.desc
index 97565815465..c17950bade2 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test3.desc
@@ -1,8 +1,9 @@
 CORE
 Test3.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string/test4.desc b/regression/strings-smoke-tests/java_int_to_string/test4.desc
index abba00197d9..e8085e4cc0b 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test4.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test4.desc
@@ -1,8 +1,9 @@
 CORE
 Test4.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string/test5.desc b/regression/strings-smoke-tests/java_int_to_string/test5.desc
index 524a176db3f..7a6c4dab79d 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test5.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test5.desc
@@ -1,8 +1,9 @@
 CORE
 Test5.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
index 416e3caec69..0d37463d104 100644
--- a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
@@ -1,8 +1,9 @@
 KNOWNBUG
 Test.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
index 20bd5377109..3b0e8c9f52e 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
@@ -1,8 +1,9 @@
 CORE
 Test_binary1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
index 370139d2c42..4b75576a9e0 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
@@ -1,8 +1,9 @@
 CORE
 Test_binary2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
index c24b0bbd20b..c0dc5a0d100 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
@@ -1,8 +1,9 @@
 CORE
 Test_binary3.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
index de106c0cbf5..5df0fa0c612 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
@@ -1,8 +1,9 @@
 CORE
 Test_decimal.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
index 48d705734ac..65d42d9d4f4 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
@@ -1,8 +1,9 @@
 CORE
 Test_hex1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
index 89c4928e147..ca27aacf182 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
@@ -1,8 +1,9 @@
 CORE
 Test_hex2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
index 0c5ff51b802..d100589824c 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
@@ -1,8 +1,9 @@
 CORE
 Test_hex3.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
index f4b1e2b219d..16600fd2a12 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
@@ -1,8 +1,9 @@
 CORE
 Test_octal1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
index aee4977a75f..cbe2eab8212 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
@@ -1,8 +1,9 @@
 CORE
 Test_octal2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
index b7a5ceb3ce1..a742982813e 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
@@ -1,8 +1,9 @@
 CORE
 Test_octal3.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
index 20efbdfa239..c81c25f146f 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
@@ -1,8 +1,9 @@
 KNOWNBUG
 Test_binary.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
index 69dbaba276d..5fec73731fc 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
@@ -1,8 +1,9 @@
 KNOWNBUG
 Test_hex.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
index 7cfc1c19f24..c47d55b6cf3 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
@@ -1,8 +1,9 @@
 KNOWNBUG
 Test_octal.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_intern/test.desc b/regression/strings-smoke-tests/java_intern/test.desc
index 58c51bce301..05b26307bb2 100644
--- a/regression/strings-smoke-tests/java_intern/test.desc
+++ b/regression/strings-smoke-tests/java_intern/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_intern.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_last_index_of/test.desc b/regression/strings-smoke-tests/java_last_index_of/test.desc
index afda4875b71..9fd0a299a7c 100644
--- a/regression/strings-smoke-tests/java_last_index_of/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of/test.desc
@@ -1,8 +1,9 @@
 CORE
 test_last_index_of.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
diff --git a/regression/strings-smoke-tests/java_last_index_of2/test.desc b/regression/strings-smoke-tests/java_last_index_of2/test.desc
index 28af8ca48e6..31f2d6afebb 100644
--- a/regression/strings-smoke-tests/java_last_index_of2/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of2/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_last_index_of2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/regression/strings-smoke-tests/java_last_index_of_char/test.desc
index aa59690787c..a1ddc2cf440 100644
--- a/regression/strings-smoke-tests/java_last_index_of_char/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of_char/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_last_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
diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc
index 7802a6d675b..59184450019 100644
--- a/regression/strings-smoke-tests/java_length/test.desc
+++ b/regression/strings-smoke-tests/java_length/test.desc
@@ -1,9 +1,10 @@
 CORE
 test_length.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[.*assertion\.1\] .* line 7 .*: SUCCESS
 \[.*assertion\.2\] .* line 8 .*: FAILURE
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_length2/test.desc b/regression/strings-smoke-tests/java_length2/test.desc
index 4647009f3cf..7223a6600d8 100644
--- a/regression/strings-smoke-tests/java_length2/test.desc
+++ b/regression/strings-smoke-tests/java_length2/test.desc
@@ -1,10 +1,12 @@
 FUTURE
 test.class
---refine-strings --string-max-length 1000 --function test.check
+--refine-strings --verbosity 10 --string-max-length 1000 --function test.check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
+--
 This test currently fails because we do not handle the case where the argument
 's' is null. This should be handled in the String model.
 The issue number for that is: diffblue/test-gen#500
diff --git a/regression/strings-smoke-tests/java_long_to_string/test1.desc b/regression/strings-smoke-tests/java_long_to_string/test1.desc
index 318ec0fb224..fd14afd9e7f 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test1.desc
@@ -1,8 +1,9 @@
 CORE
 Test1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string/test2.desc b/regression/strings-smoke-tests/java_long_to_string/test2.desc
index 1f6206fafd9..a58153ecbd5 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test2.desc
@@ -1,8 +1,9 @@
 THOROUGH
 Test2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string/test3.desc b/regression/strings-smoke-tests/java_long_to_string/test3.desc
index ea8df93a51f..4cc0e5b4f0a 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test3.desc
@@ -1,8 +1,9 @@
 THOROUGH
 Test3.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string/test4.desc b/regression/strings-smoke-tests/java_long_to_string/test4.desc
index 13dd59d749e..11df46814d6 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test4.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test4.desc
@@ -1,8 +1,9 @@
 THOROUGH
 Test4.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string/test5.desc b/regression/strings-smoke-tests/java_long_to_string/test5.desc
index 524a176db3f..7a6c4dab79d 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test5.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test5.desc
@@ -1,8 +1,9 @@
 CORE
 Test5.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
index 6f9c074face..46852f73fd8 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
@@ -1,8 +1,9 @@
 THOROUGH
 Test_binary1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
index 0729b99b895..88ecdd6658e 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
@@ -1,8 +1,9 @@
 THOROUGH
 Test_binary2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
index d87aaaecb3d..690a7051bff 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
@@ -1,8 +1,9 @@
 THOROUGH
 Test_binary3.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
index de106c0cbf5..5df0fa0c612 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
@@ -1,8 +1,9 @@
 CORE
 Test_decimal.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
index 48d705734ac..65d42d9d4f4 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
@@ -1,8 +1,9 @@
 CORE
 Test_hex1.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
index 89c4928e147..ca27aacf182 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
@@ -1,8 +1,9 @@
 CORE
 Test_hex2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
index 0c5ff51b802..d100589824c 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
@@ -1,8 +1,9 @@
 CORE
 Test_hex3.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
index 8188ebc0ee9..87aad11f09f 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
@@ -1,8 +1,9 @@
 CORE
 Test_octal1.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
index 3884ae1fa9f..11904eb55b9 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
@@ -1,8 +1,9 @@
 CORE
 Test_octal2.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
index 527357b801e..ef669e31737 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
@@ -1,8 +1,9 @@
 CORE
 Test_octal3.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
 assertion.* line 10 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint/test1.desc b/regression/strings-smoke-tests/java_parseint/test1.desc
index 5307e54205f..78d825da2ae 100644
--- a/regression/strings-smoke-tests/java_parseint/test1.desc
+++ b/regression/strings-smoke-tests/java_parseint/test1.desc
@@ -1,7 +1,9 @@
 CORE
 Test1.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 11.* FAILURE$
+--
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint/test2.desc b/regression/strings-smoke-tests/java_parseint/test2.desc
index b61e0912459..84540226f3c 100644
--- a/regression/strings-smoke-tests/java_parseint/test2.desc
+++ b/regression/strings-smoke-tests/java_parseint/test2.desc
@@ -1,7 +1,9 @@
 CORE
 Test2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 12.* FAILURE$
+--
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint/test3.desc b/regression/strings-smoke-tests/java_parseint/test3.desc
index 06f5f081dfd..f95b66184a8 100644
--- a/regression/strings-smoke-tests/java_parseint/test3.desc
+++ b/regression/strings-smoke-tests/java_parseint/test3.desc
@@ -1,6 +1,8 @@
 CORE
 Test3.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* FAILURE$
+--
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
index f66e48584e2..aa80ccad92f 100644
--- a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
@@ -1,10 +1,11 @@
 KNOWNBUG
 Test.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 13.* FAILURE$
 --
+non equal types
 --
 Issue #664 is about turning these tests on
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
index 07502efb78d..78d825da2ae 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
@@ -1,8 +1,9 @@
 CORE
 Test1.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 11.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
index 0755c7a91cf..40528a8244d 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
@@ -1,8 +1,9 @@
 CORE
 Test2.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 11.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
index ef8136a08ab..ea37ca8efb1 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
@@ -1,8 +1,9 @@
 CORE
 Test3.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 11.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
index 7934721b588..aa4756341bb 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
@@ -1,8 +1,9 @@
 CORE
 Test4.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 11.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
index a829acab959..ea45d5af377 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
@@ -1,8 +1,9 @@
 CORE
 Test5.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 11.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
index d3dadcebc8f..3ce216107c7 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
@@ -1,9 +1,10 @@
 CORE
 Test6.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 12.* FAILURE$
 --
+non equal types
 --
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
index 485ca577bcc..fe1f4d22881 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
@@ -1,10 +1,11 @@
 KNOWNBUG
 Test2.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 12.* FAILURE$
 --
+non equal types
 --
 Issue #664 is about turning these tests on
diff --git a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
index ce64f5e6db6..0271a0c984a 100644
--- a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
@@ -1,9 +1,10 @@
 CORE
 Test_binary_min.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 12.* FAILURE$
 --
+non equal types
 --
diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
index 1e195fcaaf2..640ed17fa83 100644
--- a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
@@ -1,9 +1,10 @@
 CORE
 Test_decimal_max.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 12.* FAILURE$
 --
+non equal types
 --
diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
index 7f97fa3a95e..432fa01db5b 100644
--- a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
@@ -1,9 +1,10 @@
 CORE
 Test_decimal_min.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
 ^\[.*assertion.2\].* line 12.* FAILURE$
 --
+non equal types
 --
diff --git a/regression/strings-smoke-tests/java_parselong/test_hex.desc b/regression/strings-smoke-tests/java_parselong/test_hex.desc
index c21910790b5..7dfd21113a5 100644
--- a/regression/strings-smoke-tests/java_parselong/test_hex.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_hex.desc
@@ -1,9 +1,10 @@
 CORE
 Test_hex.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 11.* FAILURE$
 --
+non equal types
 --
diff --git a/regression/strings-smoke-tests/java_parselong/test_octal.desc b/regression/strings-smoke-tests/java_parselong/test_octal.desc
index 152484b2d2a..b3310436432 100644
--- a/regression/strings-smoke-tests/java_parselong/test_octal.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_octal.desc
@@ -1,9 +1,10 @@
 CORE
 Test_octal.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 11.* FAILURE$
 --
+non equal types
 --
diff --git a/regression/strings-smoke-tests/java_replace/test.desc b/regression/strings-smoke-tests/java_replace/test.desc
index 542ed1630b5..a8536074098 100644
--- a/regression/strings-smoke-tests/java_replace/test.desc
+++ b/regression/strings-smoke-tests/java_replace/test.desc
@@ -1,10 +1,12 @@
 FUTURE
 test_replace.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
+--
 diffblue/test-gen#256
 This test is only effective with a model of
 java.lang.String.replace(LCharSequence; LCharSequence).
diff --git a/regression/strings-smoke-tests/java_replace_char/test.desc b/regression/strings-smoke-tests/java_replace_char/test.desc
index 9cf3b2fbced..ba11fa1f7e5 100644
--- a/regression/strings-smoke-tests/java_replace_char/test.desc
+++ b/regression/strings-smoke-tests/java_replace_char/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_replace_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
diff --git a/regression/strings-smoke-tests/java_set_char_at/test.desc b/regression/strings-smoke-tests/java_set_char_at/test.desc
index 72f26dda255..bfb3be131a5 100644
--- a/regression/strings-smoke-tests/java_set_char_at/test.desc
+++ b/regression/strings-smoke-tests/java_set_char_at/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_set_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
diff --git a/regression/strings-smoke-tests/java_set_length/test.desc b/regression/strings-smoke-tests/java_set_length/test.desc
index d19eb265fa4..92b178f222a 100644
--- a/regression/strings-smoke-tests/java_set_length/test.desc
+++ b/regression/strings-smoke-tests/java_set_length/test.desc
@@ -1,9 +1,10 @@
 CORE
 test_set_length.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* SUCCESS$
 ^\[.*assertion.3\].* line 10.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_starts_with/test.desc b/regression/strings-smoke-tests/java_starts_with/test.desc
index 5c62d2f2718..96348e08f11 100644
--- a/regression/strings-smoke-tests/java_starts_with/test.desc
+++ b/regression/strings-smoke-tests/java_starts_with/test.desc
@@ -1,8 +1,9 @@
 CORE
 test_starts_with.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
diff --git a/regression/strings-smoke-tests/java_string_builder_length/test.desc b/regression/strings-smoke-tests/java_string_builder_length/test.desc
index 3ad293630e3..8fbbb04690c 100644
--- a/regression/strings-smoke-tests/java_string_builder_length/test.desc
+++ b/regression/strings-smoke-tests/java_string_builder_length/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_sb_length.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_string_printable/test.desc b/regression/strings-smoke-tests/java_string_printable/test.desc
index 9a91eb68f6e..14b0a94e55d 100644
--- a/regression/strings-smoke-tests/java_string_printable/test.desc
+++ b/regression/strings-smoke-tests/java_string_printable/test.desc
@@ -1,8 +1,9 @@
 CORE
 Test.class
---refine-strings --function Test.check --string-max-length 100 --string-printable --java-assume-inputs-non-null
+--refine-strings --verbosity 10 --function Test.check --string-max-length 100 --string-printable --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file Test.java line 6 .* SUCCESS
 assertion.* file Test.java line 8 .* FAILURE
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_string_printable/test_char.desc b/regression/strings-smoke-tests/java_string_printable/test_char.desc
index af03ad6fbbe..8447c321008 100644
--- a/regression/strings-smoke-tests/java_string_printable/test_char.desc
+++ b/regression/strings-smoke-tests/java_string_printable/test_char.desc
@@ -1,7 +1,8 @@
 CORE
 Test.class
---refine-strings --function Test.check_char --string-max-length 100 --string-printable
+--refine-strings --verbosity 10 --function Test.check_char --string-max-length 100 --string-printable
 ^EXIT=0$
 ^SIGNAL=0$
 assertion.* file Test.java line 18 .* SUCCESS
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_subsequence/test.desc b/regression/strings-smoke-tests/java_subsequence/test.desc
index 3f4941d15dd..b0949a841ea 100644
--- a/regression/strings-smoke-tests/java_subsequence/test.desc
+++ b/regression/strings-smoke-tests/java_subsequence/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_subsequence.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_substring/test.desc b/regression/strings-smoke-tests/java_substring/test.desc
index 9faeee00d73..762b0237086 100644
--- a/regression/strings-smoke-tests/java_substring/test.desc
+++ b/regression/strings-smoke-tests/java_substring/test.desc
@@ -1,7 +1,8 @@
 CORE
 test_substring.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_trim/test.desc b/regression/strings-smoke-tests/java_trim/test.desc
index 171ada28356..94142169895 100644
--- a/regression/strings-smoke-tests/java_trim/test.desc
+++ b/regression/strings-smoke-tests/java_trim/test.desc
@@ -1,8 +1,9 @@
 CORE
 test_trim.class
---refine-strings --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_value_of_float/test.desc b/regression/strings-smoke-tests/java_value_of_float/test.desc
index 4e3e8769be6..ed1f8baf6e3 100644
--- a/regression/strings-smoke-tests/java_value_of_float/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float/test.desc
@@ -1,8 +1,9 @@
 CORE
 test.class
---refine-strings --function test.check --string-max-length 100
+--refine-strings --verbosity 10 --function test.check --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 7 .* SUCCESS$
 assertion.* file test.java line 9 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.desc b/regression/strings-smoke-tests/java_value_of_float_2/test.desc
index 370b9327f58..7eaf4f137af 100644
--- a/regression/strings-smoke-tests/java_value_of_float_2/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_2/test.desc
@@ -1,8 +1,9 @@
 KNOWNBUG
 test.class
---refine-strings --function test.check --string-max-length 1000
+--refine-strings --verbosity 10 --function test.check --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$
 assertion.* file test.java line 7 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.desc b/regression/strings-smoke-tests/java_value_of_float_3/test.desc
index 2c28aafd4d9..a92486ab894 100644
--- a/regression/strings-smoke-tests/java_value_of_float_3/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_3/test.desc
@@ -1,9 +1,9 @@
 KNOWNBUG
 test.class
---refine-strings --string-max-length 1000 --function test.check
+--refine-strings --verbosity 10 --string-max-length 1000 --function test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 7 .* SUCCESS$
 assertion.* file test.java line 8 .* FAILURE$
-
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.desc b/regression/strings-smoke-tests/java_value_of_float_4/test.desc
index a85559c560e..e170694c992 100644
--- a/regression/strings-smoke-tests/java_value_of_float_4/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_4/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 test.class
---refine-strings --string-max-length 1000 --function test.check
+--refine-strings --verbosity 10 --string-max-length 1000 --function test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* test.java line 8 .* SUCCESS$
@@ -8,3 +8,4 @@ assertion.* test.java line 9 .* SUCCESS$
 assertion.* test.java line 10 .* SUCCESS$
 assertion.* test.java line 11 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.desc b/regression/strings-smoke-tests/java_value_of_float_5/test.desc
index 07a7bd7edde..d643bd88a4b 100644
--- a/regression/strings-smoke-tests/java_value_of_float_5/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_5/test.desc
@@ -1,8 +1,9 @@
 THOROUGH
 test.class
---refine-strings --string-max-length 1000 --function test.check
+--refine-strings --verbosity 10 --string-max-length 1000 --function test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$
 assertion.* file test.java line 7 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc
index c7ea25ab2f8..e4e7094d764 100644
--- a/regression/strings-smoke-tests/java_value_of_long/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_long/test.desc
@@ -1,8 +1,9 @@
 CORE
 test.class
---refine-strings --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 9 .* SUCCESS$
 assertion.* file test.java line 14 .* FAILURE$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
index 7bc3ccc6c86..01640d0a77c 100644
--- a/regression/strings-smoke-tests/max_input_length/MemberTest.desc
+++ b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
@@ -1,7 +1,8 @@
 CORE
 MemberTest.class
---refine-strings --string-max-length 29 --java-assume-inputs-non-null
+--refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/max_input_length/test.desc b/regression/strings-smoke-tests/max_input_length/test.desc
index 0fddf482a9c..fb57067e0d7 100644
--- a/regression/strings-smoke-tests/max_input_length/test.desc
+++ b/regression/strings-smoke-tests/max_input_length/test.desc
@@ -1,7 +1,8 @@
 CORE
 Test.class
---refine-strings --string-max-length 30
+--refine-strings --verbosity 10 --string-max-length 30
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/max_input_length/test1.desc b/regression/strings-smoke-tests/max_input_length/test1.desc
index 00bda639119..c5252f6c564 100644
--- a/regression/strings-smoke-tests/max_input_length/test1.desc
+++ b/regression/strings-smoke-tests/max_input_length/test1.desc
@@ -1,7 +1,8 @@
 CORE
 Test.class
---refine-strings --string-max-length 45  --string-max-input-length 31
+--refine-strings --verbosity 10 --string-max-length 45  --string-max-input-length 31
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+non equal types
diff --git a/regression/strings-smoke-tests/max_input_length/test2.desc b/regression/strings-smoke-tests/max_input_length/test2.desc
index 8aaaf205c92..0edaf226ccc 100644
--- a/regression/strings-smoke-tests/max_input_length/test2.desc
+++ b/regression/strings-smoke-tests/max_input_length/test2.desc
@@ -1,7 +1,8 @@
 CORE
 Test.class
---refine-strings --string-max-length 45 --string-max-input-length 20
+--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+non equal types
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 670f933f8f6..ab747030d60 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "rational_tools.h"
 #include "config.h"
 #include "base_type.h"
+#include "type_eq.h"
 #include "namespace.h"
 #include "threeval.h"
 #include "pointer_predicates.h"
@@ -214,7 +215,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
   }
 
   // eliminate redundant typecasts
-  if(base_type_eq(expr.type(), expr.op0().type(), ns))
+  if(type_eq(expr.type(), expr.op0().type(), ns))
   {
     exprt tmp;
     tmp.swap(expr.op0());
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index a6ac35ca008..421d6a85744 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "std_expr.h"
 #include "pointer_offset_size.h"
 #include "arith_tools.h"
+#include "base_type.h"
 
 bool simplify_exprt::simplify_member(exprt &expr)
 {
@@ -208,6 +209,17 @@ bool simplify_exprt::simplify_member(exprt &expr)
       }
     }
   }
+  else if(op.id() == ID_typecast)
+  {
+    // Try to look through member(cast(x)) if the cast is between structurally
+    // identical types:
+    if(base_type_eq(op_type, op.op0().type(), ns))
+    {
+      expr.op0() = op.op0();
+      simplify_member(expr);
+      return false;
+    }
+  }
   else if(op.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(op);