diff --git a/jbmc/regression/jbmc/covered1/covered1.class b/jbmc/regression/jbmc-cover/covered1/covered1.class
similarity index 100%
rename from jbmc/regression/jbmc/covered1/covered1.class
rename to jbmc/regression/jbmc-cover/covered1/covered1.class
diff --git a/jbmc/regression/jbmc/covered1/covered1.java b/jbmc/regression/jbmc-cover/covered1/covered1.java
similarity index 100%
rename from jbmc/regression/jbmc/covered1/covered1.java
rename to jbmc/regression/jbmc-cover/covered1/covered1.java
diff --git a/jbmc/regression/jbmc/covered1/test.desc b/jbmc/regression/jbmc-cover/covered1/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/covered1/test.desc
rename to jbmc/regression/jbmc-cover/covered1/test.desc
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest.class b/jbmc/regression/jbmc-cover/generics/AbstractTest.class
deleted file mode 100644
index d2fff4e9d81..00000000000
Binary files a/jbmc/regression/jbmc-cover/generics/AbstractTest.class and /dev/null differ
diff --git a/jbmc/regression/jbmc-cover/generics/test.desc b/jbmc/regression/jbmc-cover/generics/test.desc
deleted file mode 100644
index 0fe333922c8..00000000000
--- a/jbmc/regression/jbmc-cover/generics/test.desc
+++ /dev/null
@@ -1,9 +0,0 @@
-CORE
-AbstractTest.class
---cover location --function AbstractTest.getFromAbstract
-^EXIT=0$
-^SIGNAL=0$
-file AbstractTest.java line 18 .* SATISFIED
-file AbstractTest.java line 19 .* SATISFIED
-file AbstractTest.java line 20 .* SATISFIED
-file AbstractTest.java line 21 .* SATISFIED
diff --git a/jbmc/regression/jbmc/json_trace2/Test.class b/jbmc/regression/jbmc-cover/json_trace2/Test.class
similarity index 100%
rename from jbmc/regression/jbmc/json_trace2/Test.class
rename to jbmc/regression/jbmc-cover/json_trace2/Test.class
diff --git a/jbmc/regression/jbmc/json_trace2/Test.java b/jbmc/regression/jbmc-cover/json_trace2/Test.java
similarity index 100%
rename from jbmc/regression/jbmc/json_trace2/Test.java
rename to jbmc/regression/jbmc-cover/json_trace2/Test.java
diff --git a/jbmc/regression/jbmc/json_trace2/test.desc b/jbmc/regression/jbmc-cover/json_trace2/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/json_trace2/test.desc
rename to jbmc/regression/jbmc-cover/json_trace2/test.desc
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class
index 08c0c549955..8b1f79ecc44 100644
Binary files a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class and b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java
index 552cfeb835e..91d9fe7f9a2 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java
+++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java
@@ -18,7 +18,9 @@ public String det()
         builder.setCharAt(11, ':');
         builder.setCharAt(16, ':');
         builder.setCharAt(18, ':');
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String nonDet(String s, char c, int i)
@@ -42,7 +44,9 @@ public String nonDet(String s, char c, int i)
         builder.setCharAt(11, ':');
         builder.setCharAt(16, ':');
         builder.setCharAt(18, ':');
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String withDependency(boolean b)
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc
index 668e84a1adc..68e11b514ac 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc
@@ -3,8 +3,8 @@ Test.class
 --function Test.withDependency --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 55 .*: SUCCESS
-assertion at file Test.java line 57 .*: FAILURE
+assertion at file Test.java line 59 .*: SUCCESS
+assertion at file Test.java line 61 .*: FAILURE
 --
 --
 Check that when a dependency is present, the correct constraints are added
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc
index 270ef7d2867..d3601cc9d50 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.det  --verbosity 10 --cover location
-^EXIT=0$
+--function Test.det --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 21 .*: SATISFIED
+assertion at file Test.java line 22 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc
index a76880a6c16..f5d9e0530f1 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000
-^EXIT=0$
+--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 45 .*: SATISFIED
+assertion at file Test.java line 48 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class
index 800af2c1930..77809929c05 100644
Binary files a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class and b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java
index 3caa33d3377..b4100437357 100644
--- a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java
+++ b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java
@@ -7,7 +7,9 @@ public String det()
         builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toLowerCase());
         builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toLowerCase());
         builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toLowerCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String nonDet(String s)
@@ -25,7 +27,9 @@ public String nonDet(String s)
         builder.append(":");
         builder.append(s.toLowerCase());
         builder.append(s.toLowerCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String withDependency(String s, boolean b)
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
index 6015585d6e8..8b687a7d7f2 100644
--- a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
+++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
@@ -3,8 +3,8 @@ Test.class
 --function Test.withDependency  --verbosity 10 --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 44 .*: SUCCESS
-assertion at file Test.java line 46 .*: FAILURE
+assertion at file Test.java line 48 .*: SUCCESS
+assertion at file Test.java line 50 .*: FAILURE
 --
 --
 Check that when there are dependencies, axioms are adde correctly.
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc
index eadefb44241..4b65fecb2d1 100644
--- a/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc
+++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.det  --verbosity 10 --cover location
-^EXIT=0$
+--function Test.det  --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 9 .*: SATISFIED
+assertion at file Test.java line 11 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc
index 30ef54cd492..f742265fe78 100644
--- a/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc
+++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.nonDet  --verbosity 10 --cover location --max-nondet-string-length 1000
-^EXIT=0$
+--function Test.nonDet  --verbosity 10 --max-nondet-string-length 1000
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 27 .*: SATISFIED
+assertion at file Test.java line 31 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class
index 91c3f958e3a..7aa5931dbad 100644
Binary files a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class and b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java
index 110eb7a1146..f218b183693 100644
--- a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java
+++ b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java
@@ -7,7 +7,9 @@ public String det()
         builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase());
         builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase());
         builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String nonDet(String s)
@@ -25,7 +27,9 @@ public String nonDet(String s)
         builder.append(":");
         builder.append(s.toUpperCase());
         builder.append(s.toUpperCase());
-        return builder.toString();
+        String result = builder.toString();
+        assert result.length() < 5;
+        return result;
     }
 
     public String withDependency(String s, boolean b)
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc
index 472de29b000..cd4f2cd1745 100644
--- a/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc
+++ b/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc
@@ -3,8 +3,8 @@ Test.class
 --function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 44 .*: SUCCESS
-assertion at file Test.java line 46 .*: FAILURE
+assertion at file Test.java line 48 .*: SUCCESS
+assertion at file Test.java line 50 .*: FAILURE
 --
 --
 Check that when there are dependencies, axioms are added correctly.
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc
index eadefb44241..4b65fecb2d1 100644
--- a/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc
+++ b/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.det  --verbosity 10 --cover location
-^EXIT=0$
+--function Test.det  --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 9 .*: SATISFIED
+assertion at file Test.java line 11 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc
index 30ef54cd492..88a0d5e0809 100644
--- a/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc
+++ b/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.nonDet  --verbosity 10 --cover location --max-nondet-string-length 1000
-^EXIT=0$
+--function Test.nonDet --verbosity 10 --max-nondet-string-length 1000
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 27 .*: SATISFIED
+assertion at file Test.java line 31 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class
index 4ecf201f185..aaacd49ac54 100644
Binary files a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class and b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java
index 1af7317bca5..323958250a5 100644
--- a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java
+++ b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java
@@ -23,6 +23,7 @@ public static String checkDet()
         tmp = String.valueOf(-1000003);
         tmp = String.valueOf(1000004);
         tmp = String.valueOf(1000005);
+        assert tmp.length() < 5;
         return tmp;
     }
 
@@ -51,6 +52,7 @@ public static String checkNonDet(int i)
         tmp += String.valueOf(-i + 1);
         tmp += " ";
         tmp += String.valueOf(-i - 2);
+        assert tmp.length() < 5;
         return tmp;
     }
 
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc
index 18c4b3b0f9a..23646edbe11 100644
--- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc
+++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc
@@ -3,8 +3,8 @@ Test.class
 --function Test.checkWithDependency --depth 10000
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 61 .*: SUCCESS
-assertion at file Test.java line 64 .*: FAILURE
+assertion at file Test.java line 63 .*: SUCCESS
+assertion at file Test.java line 66 .*: FAILURE
 --
 --
 Check that when a dependency is present, the correct constraints are added
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc
index 8fc14e7e524..fe9947fcaa7 100644
--- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc
+++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.checkDet --verbosity 10 --cover location
-^EXIT=0$
+--function Test.checkDet --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 25 .*: SATISFIED
+assertion at file Test.java line 26 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc
index 7342d08a711..5d31175c3b9 100644
--- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc
+++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc
@@ -1,9 +1,9 @@
 CORE
 Test.class
---function Test.checkNonDet --verbosity 10 --cover location
-^EXIT=0$
+--function Test.checkNonDet --verbosity 10
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* file Test.java line 53 .*: SATISFIED
+assertion at file Test.java line 55 .*: FAILURE
 --
 adding lemma .*nondet_infinite_array
 --
diff --git a/jbmc/regression/jbmc-strings/char_escape/Test.class b/jbmc/regression/jbmc-strings/char_escape/Test.class
index 5ffa97543e0..f866609afb5 100644
Binary files a/jbmc/regression/jbmc-strings/char_escape/Test.class and b/jbmc/regression/jbmc-strings/char_escape/Test.class differ
diff --git a/jbmc/regression/jbmc-strings/char_escape/Test.java b/jbmc/regression/jbmc-strings/char_escape/Test.java
index 791563bbbc0..467e0f838e6 100644
--- a/jbmc/regression/jbmc-strings/char_escape/Test.java
+++ b/jbmc/regression/jbmc-strings/char_escape/Test.java
@@ -10,10 +10,15 @@ public static boolean test(char c1, char c2, char c3, char c4, char c5, char c6,
         sb.append(c6);
         sb.append(c7);
         sb.append(c8);
-        if (sb.toString().equals("\b\t\n\f\r\"\'\\"))
+        if (sb.toString().equals("\b\t\n\f\r\"\'\\")) {
+            assert false;
             return true;
-        if (!sb.toString().equals("\b\t\n\f\r\"\'\\"))
+        }
+        if (!sb.toString().equals("\b\t\n\f\r\"\'\\")) {
+            assert false;
             return false;
+        }
+        assert false;
         return true;
     }
 }
diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc
index 46c23067a93..d25b7391444 100644
--- a/jbmc/regression/jbmc-strings/char_escape/test.desc
+++ b/jbmc/regression/jbmc-strings/char_escape/test.desc
@@ -1,6 +1,9 @@
 CORE
 Test.class
---function Test.test --cover location --trace --json-ui
-^EXIT=0$
+--function Test.test --trace --json-ui
+^EXIT=10$
 ^SIGNAL=0$
-20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)
+"reason": "assertion at file Test.java line 14
+"reason": "assertion at file Test.java line 18
+--
+"reason": "assertion at file Test.java line 21
diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class
index 6120bff5bb6..0b37d96013b 100644
Binary files a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class and b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.class differ
diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java
index c57b3e19be8..ad81b8ac686 100644
--- a/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java
+++ b/jbmc/regression/jbmc-strings/max-length-generic-array/IntegerTests.java
@@ -4,7 +4,11 @@ public static Boolean testMyGenSet(Integer key) {
         if (key == null) return null;
         MyGenSet<Integer> ms = new MyGenSet<>();
         ms.array[0] = 101;
-        if (ms.contains(key)) return true;
+        if (ms.contains(key)) {
+          assert false;
+          return true;
+        }
+        assert false;
         return false;
     }
 
@@ -12,7 +16,11 @@ public static Boolean testMySet(Integer key) {
         if (key == null) return null;
         MySet ms = new MySet();
         ms.array[0] = 101;
-        if (ms.contains(key)) return true;
+        if (ms.contains(key)) {
+          assert false;
+          return true;
+        }
+        assert false;
         return false;
     }
 
diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class b/jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class
index e92e43fee85..d7dc326cc8a 100644
Binary files a/jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class and b/jbmc/regression/jbmc-strings/max-length-generic-array/MyGenSet.class differ
diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/MySet.class b/jbmc/regression/jbmc-strings/max-length-generic-array/MySet.class
index e890519fb8b..2f7e7ae2d75 100644
Binary files a/jbmc/regression/jbmc-strings/max-length-generic-array/MySet.class and b/jbmc/regression/jbmc-strings/max-length-generic-array/MySet.class differ
diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc
index e712029ce44..56373bd9be5 100644
--- a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc
+++ b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc
@@ -1,19 +1,7 @@
 CORE
 IntegerTests.class
---max-nondet-string-length 100 --function IntegerTests.testMySet --cover location
-^EXIT=0$
+--max-nondet-string-length 100 --function IntegerTests.testMySet
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED
-coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED
-coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED
-coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED
-coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED
-coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED
-coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED
-coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED
-coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED
-coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED
-coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED
+assertion at file IntegerTests.java line 20 .*: FAILURE
+assertion at file IntegerTests.java line 23 .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc
index ca374b5183c..1e86880a323 100644
--- a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc
+++ b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc
@@ -1,20 +1,7 @@
 CORE
 IntegerTests.class
---max-nondet-string-length 100 --function IntegerTests.testMyGenSet --cover location
-^EXIT=0$
+--max-nondet-string-length 100 --function IntegerTests.testMyGenSet
+^EXIT=10$
 ^SIGNAL=0$
-coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED
-coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED
-coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED
-coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED
-coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED
-coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED
-coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED
-coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED
-coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED
-coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED
-coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED
-coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED
+assertion at file IntegerTests.java line 8 .*: FAILURE
+assertion at file IntegerTests.java line 11 .*: FAILURE
diff --git a/jbmc/regression/jbmc/array2/test.class b/jbmc/regression/jbmc/array2/test.class
index 507d6622e5c..10fc89c0a68 100644
Binary files a/jbmc/regression/jbmc/array2/test.class and b/jbmc/regression/jbmc/array2/test.class differ
diff --git a/jbmc/regression/jbmc/array2/test.desc b/jbmc/regression/jbmc/array2/test.desc
index 4998d1faa84..66451742da5 100644
--- a/jbmc/regression/jbmc/array2/test.desc
+++ b/jbmc/regression/jbmc/array2/test.desc
@@ -1,7 +1,6 @@
 CORE
 test.class
---function test.f --cover location
-\d+ of \d+ covered
+--function test.f
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/array2/test.java b/jbmc/regression/jbmc/array2/test.java
index 075017405ee..c0542f5ccf3 100644
--- a/jbmc/regression/jbmc/array2/test.java
+++ b/jbmc/regression/jbmc/array2/test.java
@@ -11,6 +11,10 @@ public void f(int unknown) {
     if(unknown > 0)
       arr[0]=1;
 
+    if(unknown > 0)
+      assert arr[0] == 1;
+    else
+      assert arr.length == 0;
   }
 
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class
index e31a62ef61b..14f1d91ebe7 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class
index f894ebdb1e0..ba36f3ebae8 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java
index b631e2e7617..4df7453e41f 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java
@@ -1,7 +1,8 @@
 public class FloatMultidim1 {
   public float[][] f(int y) {
+    float[][] a1 = null;
     if (y > 0 && y < 5) {
-      float[][] a1 = new float[y][2];
+      a1 = new float[y][2];
       int j;
       if (y > 1) {
         j = 1;
@@ -9,9 +10,8 @@ public float[][] f(int y) {
         j = 0;
       }
       a1[j][1] = 1.0f;
-      return a1;
-    } else {
-      return null;
     }
+    assert a1 == null;
+    return a1;
   }
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class
index 4d40ffc3741..a2ca10913d1 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java
index 6d80d3b38c5..4fd9d37a25a 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java
@@ -1,7 +1,8 @@
 public class FloatMultidim2 {
   public float[][] f(int y) {
+    float[][] a1 = null;
     if (y > 0 && y < 5) {
-      float[][] a1 = new float[2][y];
+      a1 = new float[2][y];
       int j;
       if (y > 1) {
         j = 1;
@@ -9,9 +10,8 @@ public float[][] f(int y) {
         j = 0;
       }
       a1[1][j] = 1.0f;
-      return a1;
-    } else {
-      return new float[1][1];
     }
+    assert a1 == null;
+    return a1;
   }
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class
index 4102562d05f..38ea3340b0c 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java
index 58ed13eaaa4..2c00d0f5cb4 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java
@@ -1,7 +1,8 @@
 public class RefMultidim1 {
   public A[][] f(int y) {
+    A[][] a1 = null;
     if (y > 0 && y < 5) {
-      A[][] a1 = new A[y][2];
+      a1 = new A[y][2];
       int j;
       if (y > 1) {
         j = 1;
@@ -10,9 +11,8 @@ public A[][] f(int y) {
       }
       a1[j][1] = new A();
       a1[j][1].a = 1.0f;
-      return a1;
-    } else {
-      return null;
     }
+    assert a1 == null;
+    return a1;
   }
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class
index fa85a072b9f..f55c4cdf726 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java
index ae5be7d1ecd..acdb7b79f32 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java
@@ -1,7 +1,8 @@
 public class RefMultidim2 {
   public A[][] f(int y) {
+    A[][] a1 = null;
     if (y > 0 && y < 5) {
-      A[][] a1 = new A[2][y];
+      a1 = new A[2][y];
       int j;
       if (y > 1) {
         j = 1;
@@ -10,9 +11,8 @@ public A[][] f(int y) {
       }
       a1[1][j] = new A();
       a1[1][j].a = 1.0f;
-      return a1;
-    } else {
-      return null;
     }
+    assert a1 == null;
+    return a1;
   }
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class
index c474465f50d..1287e3d6ba6 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java
index 90692e0392a..fc8fe3bcc2a 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java
@@ -4,5 +4,6 @@ public void f(int y) {
     int j = 1;
     a1[j][1] = new A();
     a1[j][1].a = 1.0f;
+    assert a1[1][j] == null;
   }
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class
index 741443d1e2d..e3a1a32b818 100644
Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class and b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class differ
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java
index 1237623d6f5..4e3a081738f 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java
@@ -1,7 +1,8 @@
 public class RefSingledim {
   public A[] f(int y) {
+    A[] a1 = null;
     if (y > 0 && y < 5) {
-      A[] a1 = new A[y];
+      a1 = new A[y];
       int j;
       if (y > 1) {
         j = 1;
@@ -10,9 +11,8 @@ public A[] f(int y) {
       }
       a1[j] = new A();
       a1[j].a = 1.0f;
-      return a1;
-    } else {
-      return null;
     }
+    assert a1 == null;
+    return a1;
   }
 }
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc
index 98169774c6f..f1cd44420c8 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc
@@ -1,9 +1,6 @@
 CORE
 FloatMultidim1.class
---function FloatMultidim1.f --cover location --unwind 3
-\d+ of \d+ covered
-^EXIT=0$
+--function FloatMultidim1.f --unwind 3
+^EXIT=10$
 ^SIGNAL=0$
-y=1$
-y=[2-4]$
-y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
+assertion at file FloatMultidim1.java line 14 .*: FAILURE
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc
index 9f1c5d4581b..09f87e5d867 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc
@@ -1,8 +1,6 @@
 CORE
 FloatMultidim2.class
---function FloatMultidim2.f --cover location --unwind 3
-^EXIT=0$
+--function FloatMultidim2.f --unwind 3
+^EXIT=10$
 ^SIGNAL=0$
-y=1$
-y=[2-4]$
-y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
+assertion at file FloatMultidim2.java line 14 .*: FAILURE
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc
index c4a07a7c56b..0ff8489c7d4 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc
@@ -1,9 +1,6 @@
 CORE
 RefMultidim1.class
---function RefMultidim1.f --cover location --unwind 3
-\d+ of \d+ covered
-^EXIT=0$
+--function RefMultidim1.f --unwind 3
+^EXIT=10$
 ^SIGNAL=0$
-y=1$
-y=[2-4]$
-y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
+assertion at file RefMultidim1.java line 15 .*: FAILURE
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc
index 1f46e69a206..ee16addfad0 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc
@@ -1,9 +1,6 @@
 CORE
 RefMultidim2.class
---function RefMultidim2.f --cover location --unwind 3
-\d+ of \d+ covered
-^EXIT=0$
+--function RefMultidim2.f --unwind 3
+^EXIT=10$
 ^SIGNAL=0$
-y=1$
-y=[2-4]$
-y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
+assertion at file RefMultidim2.java line 15 .*: FAILURE
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc
index eeb64c3e6b1..c054f7ad4ef 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc
@@ -1,6 +1,6 @@
 CORE
 RefMultidimConstsize.class
---function RefMultidimConstsize.f --cover location --unwind 3
-^EXIT=0$
+--function RefMultidimConstsize.f --unwind 3
+^EXIT=10$
 ^SIGNAL=0$
-y=-*[0-9]+$
+assertion at file RefMultidimConstsize.java line 7 .*: FAILURE
diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc
index 84db685c705..6276db8f31e 100644
--- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc
+++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc
@@ -1,8 +1,6 @@
 CORE
 RefSingledim.class
---function RefSingledim.f --cover location --unwind 3
-^EXIT=0$
+--function RefSingledim.f --unwind 3
+^EXIT=10$
 ^SIGNAL=0$
-y=1$
-y=[2-4]$
-y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
+assertion at file RefSingledim.java line 15 .*: FAILURE
diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.class b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.class
index 66e0d073242..0db5253f489 100644
Binary files a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.class and b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.class differ
diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java
index 16d680bd804..66051d5fc3b 100644
--- a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java
+++ b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/TestClass.java
@@ -1,7 +1,10 @@
 public class TestClass {
   public static void f(int y) {
+    if(y < 1)
+      return;
     float[][] a1 = new float[y][3];
     int j = 0;
     a1[j][0] = 34.5f;
+    assert a1[0][j] > 0;
   }
 }
diff --git a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc
index a4220527596..73caffc0a7d 100644
--- a/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc
+++ b/jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc
@@ -1,5 +1,8 @@
 CORE
 TestClass.class
---function TestClass.f --cover location --unwind 2
+--function TestClass.f --unwind 2
 ^EXIT=0$
 ^SIGNAL=0$
+--
+--
+Tests that there is no crash.
diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class
index 56f0ef4b05a..b9f700ea97d 100644
Binary files a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class and b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class differ
diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class
index c7dfc05289a..5373625244f 100644
Binary files a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class and b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class differ
diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java
index af6f1bfdcf0..b3c590686a6 100644
--- a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java
+++ b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java
@@ -5,12 +5,16 @@ public int foo(MyEnum e) {
     if (e == null) return 0;
     switch (e) {
       case A:
+        assert false;
         return 1;
       case B:
+        assert false;
         return 2;
       case C:
+        assert false;
         return 3;
     }
+    assert false;
     return 5;
   }
 }
diff --git a/jbmc/regression/jbmc/enum_switch/test.desc b/jbmc/regression/jbmc/enum_switch/test.desc
index f525e3e15d4..6001b0456fb 100644
--- a/jbmc/regression/jbmc/enum_switch/test.desc
+++ b/jbmc/regression/jbmc/enum_switch/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/Foo.class
---trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
-line 8.*SATISFIED
-line 10.*SATISFIED
-line 12.*SATISFIED
-line 14.*SATISFIED
-^EXIT=0$
+--trace --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
+assertion at file com/diffblue/regression/Foo.java line 8 .*: FAILURE
+assertion at file com/diffblue/regression/Foo.java line 11 .*: FAILURE
+assertion at file com/diffblue/regression/Foo.java line 14 .*: FAILURE
+assertion at file com/diffblue/regression/Foo.java line 17 .*: FAILURE
+^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class
index e977adcf00c..6e778a9c7ac 100644
Binary files a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class and b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class differ
diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java
index bc5d1f617b6..341ad8a6ee8 100644
--- a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java
+++ b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java
@@ -1,8 +1,8 @@
 package com.diffblue.regression;
 public class EnumIter {
-    int f() {
+    void f() {
         MyEnum[] a = MyEnum.values();
         int num = a[2].ordinal() + a[3].ordinal();
-        return num ;
+        assert num == 5;
     }
 }
diff --git a/jbmc/regression/jbmc/enum_values_clone/test.desc b/jbmc/regression/jbmc/enum_values_clone/test.desc
index 7009afb0ed1..3d6fc869747 100644
--- a/jbmc/regression/jbmc/enum_values_clone/test.desc
+++ b/jbmc/regression/jbmc/enum_values_clone/test.desc
@@ -1,7 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/EnumIter.class
---trace  --cover location --depth 1024  --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
-\d+ of \d+ covered \(100\.0%\)
+--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class
index 3c7ca188bc9..f0733f1749d 100644
Binary files a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class and b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class differ
diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java
index 4dcfdfca3d2..16e32d1cc31 100644
--- a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java
+++ b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java
@@ -1,7 +1,8 @@
 package com.diffblue.regression;
 public class EnumIter {
-    String f() {
+    void f() {
         MyEnum[] a = MyEnum.values();
-        return a[2].name() + a[3].name();
+        String s = a[2].name() + a[3].name();
+        assert s.equals("CD");
     }
 }
diff --git a/jbmc/regression/jbmc/enum_values_clone_name/test.desc b/jbmc/regression/jbmc/enum_values_clone_name/test.desc
index 66031ef1e9d..3d6fc869747 100644
--- a/jbmc/regression/jbmc/enum_values_clone_name/test.desc
+++ b/jbmc/regression/jbmc/enum_values_clone_name/test.desc
@@ -1,7 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/EnumIter.class
---trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
-\d+ of \d+ covered \(100\.0%\)
+--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/generic_class_bound1/Gn.class b/jbmc/regression/jbmc/generic_class_bound1/Gn.class
index 5513d09916c..046d3a9fe66 100644
Binary files a/jbmc/regression/jbmc/generic_class_bound1/Gn.class and b/jbmc/regression/jbmc/generic_class_bound1/Gn.class differ
diff --git a/jbmc/regression/jbmc/generic_class_bound1/Gn.java b/jbmc/regression/jbmc/generic_class_bound1/Gn.java
index 5dfbf4da153..8b48f7742cf 100644
--- a/jbmc/regression/jbmc/generic_class_bound1/Gn.java
+++ b/jbmc/regression/jbmc/generic_class_bound1/Gn.java
@@ -7,9 +7,11 @@ public class Gn<T extends L<? extends B>>{
 	Gn<?> ex1;
 	public void foo1(Gn<?> ex1){
 		if(ex1 != null)
-		this.ex1 = ex1;
+		    this.ex1 = ex1;
+		assert false;
 	}
 	public static void main(String[] args) {
 		System.out.println("ddfsdf");
+		assert false;
 	}
 }
diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/jbmc/regression/jbmc/generic_class_bound1/test.desc
index 6f623851472..e7de31a26cd 100644
--- a/jbmc/regression/jbmc/generic_class_bound1/test.desc
+++ b/jbmc/regression/jbmc/generic_class_bound1/test.desc
@@ -1,12 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 Gn.class
---cover location --no-lazy-methods --no-refine-strings
-^EXIT=0$
+--no-lazy-methods --no-refine-strings
+^EXIT=10$
 ^SIGNAL=0$
-.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED
-.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block .: FAILED
-.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block .: FAILED
-.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block .: SATISFIED
+.*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V.*SUCCESS
+.*file Gn.java line 15 function java::Gn.main:\(\[Ljava/lang/String;\)V.*FAILURE
 --
 --
 This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractImpl.class b/jbmc/regression/jbmc/generics/AbstractImpl.class
similarity index 100%
rename from jbmc/regression/jbmc-cover/generics/AbstractImpl.class
rename to jbmc/regression/jbmc/generics/AbstractImpl.class
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractInt.class b/jbmc/regression/jbmc/generics/AbstractInt.class
similarity index 100%
rename from jbmc/regression/jbmc-cover/generics/AbstractInt.class
rename to jbmc/regression/jbmc/generics/AbstractInt.class
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest$ClassA.class b/jbmc/regression/jbmc/generics/AbstractTest$ClassA.class
similarity index 87%
rename from jbmc/regression/jbmc-cover/generics/AbstractTest$ClassA.class
rename to jbmc/regression/jbmc/generics/AbstractTest$ClassA.class
index b22a6b21506..f98494fed70 100644
Binary files a/jbmc/regression/jbmc-cover/generics/AbstractTest$ClassA.class and b/jbmc/regression/jbmc/generics/AbstractTest$ClassA.class differ
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest$ClassB.class b/jbmc/regression/jbmc/generics/AbstractTest$ClassB.class
similarity index 79%
rename from jbmc/regression/jbmc-cover/generics/AbstractTest$ClassB.class
rename to jbmc/regression/jbmc/generics/AbstractTest$ClassB.class
index bd168a70121..b060b10df5a 100644
Binary files a/jbmc/regression/jbmc-cover/generics/AbstractTest$ClassB.class and b/jbmc/regression/jbmc/generics/AbstractTest$ClassB.class differ
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest$Dummy.class b/jbmc/regression/jbmc/generics/AbstractTest$Dummy.class
similarity index 87%
rename from jbmc/regression/jbmc-cover/generics/AbstractTest$Dummy.class
rename to jbmc/regression/jbmc/generics/AbstractTest$Dummy.class
index 76f7bb61679..020090a3d48 100644
Binary files a/jbmc/regression/jbmc-cover/generics/AbstractTest$Dummy.class and b/jbmc/regression/jbmc/generics/AbstractTest$Dummy.class differ
diff --git a/jbmc/regression/jbmc/generics/AbstractTest.class b/jbmc/regression/jbmc/generics/AbstractTest.class
new file mode 100644
index 00000000000..313c1e6edf7
Binary files /dev/null and b/jbmc/regression/jbmc/generics/AbstractTest.class differ
diff --git a/jbmc/regression/jbmc-cover/generics/AbstractTest.java b/jbmc/regression/jbmc/generics/AbstractTest.java
similarity index 72%
rename from jbmc/regression/jbmc-cover/generics/AbstractTest.java
rename to jbmc/regression/jbmc/generics/AbstractTest.java
index 5b6049a211c..84e9bbcec34 100644
--- a/jbmc/regression/jbmc-cover/generics/AbstractTest.java
+++ b/jbmc/regression/jbmc/generics/AbstractTest.java
@@ -13,10 +13,15 @@ class ClassB {
         int getId() { return id; }
     }
 
-    public int getFromAbstract(AbstractInt<ClassA, ClassB> arg) {
+    public int getFromAbstract(AbstractImpl<ClassA, ClassB> arg) {
+        if (arg == null)
+            return -1;
         AbstractImpl<Dummy, Dummy> dummy = new AbstractImpl<>();
         ClassB b = arg.get();
+        if (b == null)
+            return -1;
         int i = b.getId();
+        assert(i > 0);
         return i;
     }
 }
diff --git a/jbmc/regression/jbmc/generics/test.desc b/jbmc/regression/jbmc/generics/test.desc
new file mode 100644
index 00000000000..6b2de09b2e4
--- /dev/null
+++ b/jbmc/regression/jbmc/generics/test.desc
@@ -0,0 +1,6 @@
+CORE
+AbstractTest.class
+--function AbstractTest.getFromAbstract
+^EXIT=10$
+^SIGNAL=0$
+assertion at file AbstractTest.java line 24 .*: FAILURE
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class
index a7920d988fc..87c97a68d9e 100644
Binary files a/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class and b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class differ
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class
index 58e7cc0256a..06d26000d4e 100644
Binary files a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class and b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class differ
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
index 1fbdeb644d2..d9492106c67 100644
--- a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
+++ b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
@@ -6,6 +6,7 @@ class KeyValue<K, V> {
 }
 class MutuallyRecursiveGenerics {
   void f() {
-    KeyValue<String, Integer> example1;
+    KeyValue<String, Integer> example1 = new KeyValue<>();
+    assert example1 != null;
   }
 }
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc
index 859670558b4..08f1ae52143 100644
--- a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc
+++ b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc
@@ -1,6 +1,6 @@
 CORE
 MutuallyRecursiveGenerics.class
---cover location --function MutuallyRecursiveGenerics.f
+--function MutuallyRecursiveGenerics.f
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/generics_type_param/GenericFields$SimpleGenericField.class b/jbmc/regression/jbmc/generics_type_param/GenericFields$SimpleGenericField.class
index daf2c6ff9b4..351f249110b 100644
Binary files a/jbmc/regression/jbmc/generics_type_param/GenericFields$SimpleGenericField.class and b/jbmc/regression/jbmc/generics_type_param/GenericFields$SimpleGenericField.class differ
diff --git a/jbmc/regression/jbmc/generics_type_param/GenericFields.java b/jbmc/regression/jbmc/generics_type_param/GenericFields.java
index 3b903ebaa56..59f1ccf8919 100644
--- a/jbmc/regression/jbmc/generics_type_param/GenericFields.java
+++ b/jbmc/regression/jbmc/generics_type_param/GenericFields.java
@@ -19,7 +19,9 @@ class SimpleGenericField  {
     public void foo() {
     }
     SimpleWrapper<IWrapper> f(SimpleWrapper<FWrapper> s, SimpleWrapper<AWrapper []> a) {
-      return new SimpleWrapper<>();
+      SimpleWrapper<IWrapper> r = new SimpleWrapper<>();
+      assert r != null;
+      return r;
     }
   }
 }
diff --git a/jbmc/regression/jbmc/generics_type_param/test.desc b/jbmc/regression/jbmc/generics_type_param/test.desc
index 4b4bcca0974..ef3971e4559 100644
--- a/jbmc/regression/jbmc/generics_type_param/test.desc
+++ b/jbmc/regression/jbmc/generics_type_param/test.desc
@@ -1,6 +1,6 @@
 CORE
 GenericFields$SimpleGenericField.class
---cover location --function GenericFields\$SimpleGenericField.foo --verbosity 10
+--function GenericFields\$SimpleGenericField.foo --verbosity 10
 ^EXIT=0$
 ^SIGNAL=0$
 Reading class AWrapper
diff --git a/jbmc/regression/jbmc/integer_without_simplify1/test.desc b/jbmc/regression/jbmc/integer_without_simplify1/test.desc
index 284277c7b4a..b6f6e0dc0de 100644
--- a/jbmc/regression/jbmc/integer_without_simplify1/test.desc
+++ b/jbmc/regression/jbmc/integer_without_simplify1/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---no-simplify --function test.f --cover location
+--no-simplify --function test.f
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class b/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class
index 9c810453dec..af8d3a3d7c4 100644
Binary files a/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class and b/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class differ
diff --git a/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java b/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java
index 012c3c7a355..848f387ec93 100644
--- a/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java
+++ b/jbmc/regression/jbmc/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java
@@ -20,6 +20,8 @@ public boolean hasItem() {
   public boolean setItem(Item item) {
     boolean exists = hasItem();
     this.item = item;
+
+    assert this.item == null;
     return exists;
   }
 }
diff --git a/jbmc/regression/jbmc/internal1/test.desc b/jbmc/regression/jbmc/internal1/test.desc
index 09047367ca9..cf3ffadb366 100644
--- a/jbmc/regression/jbmc/internal1/test.desc
+++ b/jbmc/regression/jbmc/internal1/test.desc
@@ -1,8 +1,8 @@
 CORE
 com/diffblue/javatest/nestedobjects/subpackage/Order.class
---json-ui --function 'com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:(Lcom/diffblue/javatest/nestedobjects/subpackage/Item;)Z' --cover location --trace
+--json-ui --function 'com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:(Lcom/diffblue/javatest/nestedobjects/subpackage/Item;)Z' --trace
 activate-multi-line-match
-EXIT=0
+EXIT=10
 SIGNAL=0
 "identifier": "__CPROVER_initialize",\n *"sourceLocation": [{][}]\n *[}],\n *"hidden": false,\n *"internal": true,\n *"stepType": "function-call",
 "internal": true,\n *"lhs": "tmp_object_factory[$][0-9]+",
diff --git a/jbmc/regression/jbmc/iterator1/iterator1.class b/jbmc/regression/jbmc/iterator1/iterator1.class
index 2a1b755c88b..8fdd5d7fb31 100644
Binary files a/jbmc/regression/jbmc/iterator1/iterator1.class and b/jbmc/regression/jbmc/iterator1/iterator1.class differ
diff --git a/jbmc/regression/jbmc/iterator1/iterator1.java b/jbmc/regression/jbmc/iterator1/iterator1.java
index 4e94534fe70..a4c06d53d7a 100644
--- a/jbmc/regression/jbmc/iterator1/iterator1.java
+++ b/jbmc/regression/jbmc/iterator1/iterator1.java
@@ -7,5 +7,7 @@ public void f(List<String> list)
     int i = 0;
     for(String s : list)
       i++;
+
+    assert false;
   }
 }
diff --git a/jbmc/regression/jbmc/iterator1/test.desc b/jbmc/regression/jbmc/iterator1/test.desc
index 3e8c6068f6a..550f9ad5e95 100644
--- a/jbmc/regression/jbmc/iterator1/test.desc
+++ b/jbmc/regression/jbmc/iterator1/test.desc
@@ -1,8 +1,10 @@
 CORE
 iterator1.class
---cover location --unwind 3 --function iterator1.f 
-^EXIT=0$
+--unwind 3 --function iterator1.f
+^EXIT=10$
 ^SIGNAL=0$
-^.*SATISFIED$
+^.*FAILURE
 --
 ^warning: ignoring
+--
+Tests that end of function is reachable.
diff --git a/jbmc/regression/jbmc/iterator2/iterator2.class b/jbmc/regression/jbmc/iterator2/iterator2.class
index 45d6532dfff..d5dddf70c78 100644
Binary files a/jbmc/regression/jbmc/iterator2/iterator2.class and b/jbmc/regression/jbmc/iterator2/iterator2.class differ
diff --git a/jbmc/regression/jbmc/iterator2/iterator2.java b/jbmc/regression/jbmc/iterator2/iterator2.java
index 16b40e48dd3..7b8369b4806 100644
--- a/jbmc/regression/jbmc/iterator2/iterator2.java
+++ b/jbmc/regression/jbmc/iterator2/iterator2.java
@@ -11,5 +11,6 @@ public void f(List<List<String>> list)
         i++;
     }
     for(j=0;j<i;j++);
+    assert false;
   }
 }
diff --git a/jbmc/regression/jbmc/iterator2/test.desc b/jbmc/regression/jbmc/iterator2/test.desc
index 1919744c42d..8939cc01f62 100644
--- a/jbmc/regression/jbmc/iterator2/test.desc
+++ b/jbmc/regression/jbmc/iterator2/test.desc
@@ -1,8 +1,10 @@
 CORE
 iterator2.class
---cover location --unwind 3 --function iterator2.f
-^EXIT=0$
+--unwind 3 --function iterator2.f
+^EXIT=10$
 ^SIGNAL=0$
-^.*SATISFIED$
+^.*FAILURE
 --
 ^warning: ignoring
+--
+Tests that end of function is reachable.
diff --git a/jbmc/regression/jbmc/json_trace1/Test.class b/jbmc/regression/jbmc/json_trace1/Test.class
index 2f57ffa3c57..169b0ca1d34 100644
Binary files a/jbmc/regression/jbmc/json_trace1/Test.class and b/jbmc/regression/jbmc/json_trace1/Test.class differ
diff --git a/jbmc/regression/jbmc/json_trace1/Test.java b/jbmc/regression/jbmc/json_trace1/Test.java
index 79cb55bfdf9..956ed099a7a 100644
--- a/jbmc/regression/jbmc/json_trace1/Test.java
+++ b/jbmc/regression/jbmc/json_trace1/Test.java
@@ -16,6 +16,7 @@ byte main(byte[] a) {
       }
     }
 
+    assert a[0] == 0;
     return -1;
   }
 }
diff --git a/jbmc/regression/jbmc/json_trace1/test.desc b/jbmc/regression/jbmc/json_trace1/test.desc
index d0f9b27b618..52971e9fbd3 100644
--- a/jbmc/regression/jbmc/json_trace1/test.desc
+++ b/jbmc/regression/jbmc/json_trace1/test.desc
@@ -1,7 +1,9 @@
 CORE
 Test.class
---cover location --trace --json-ui --function Test.main
-^EXIT=0$
+--trace --json-ui --function Test.main
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+Tests that it doesn't crash.
\ No newline at end of file
diff --git a/jbmc/regression/jbmc/json_trace3/Test.class b/jbmc/regression/jbmc/json_trace3/Test.class
index 86426242aaa..49de1083374 100644
Binary files a/jbmc/regression/jbmc/json_trace3/Test.class and b/jbmc/regression/jbmc/json_trace3/Test.class differ
diff --git a/jbmc/regression/jbmc/json_trace3/Test.java b/jbmc/regression/jbmc/json_trace3/Test.java
index 02cc993c56e..45e1b7d8c07 100644
--- a/jbmc/regression/jbmc/json_trace3/Test.java
+++ b/jbmc/regression/jbmc/json_trace3/Test.java
@@ -1,9 +1,12 @@
 public class Test {
   public static void main(long[] a) {
+    if(a == null)
+      return;
     if(a.length<3)
       return;
     for(int i=0; i<a.length; i++) {
       a[i]=(long)i;
     }
+    assert a[0] != 0;
   }
 }
diff --git a/jbmc/regression/jbmc/json_trace3/test.desc b/jbmc/regression/jbmc/json_trace3/test.desc
index 12b9216ff07..830295e9eaa 100644
--- a/jbmc/regression/jbmc/json_trace3/test.desc
+++ b/jbmc/regression/jbmc/json_trace3/test.desc
@@ -1,10 +1,10 @@
 CORE
 Test.class
---cover location --trace --json-ui --unwind 5 --function Test.main
+--trace --json-ui --unwind 5 --function Test.main
 activate-multi-line-match
-EXIT=0
+EXIT=10
 SIGNAL=0
-"lhs": "dynamic_2_array\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "15",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "6"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
+"lhs": "dynamic_2_array\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
 --
 "name": "unknown"
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/nondet-static/My$PInner.class b/jbmc/regression/jbmc/nondet-static/My$PInner.class
index 58d8d6f41f8..f99401f5dfb 100644
Binary files a/jbmc/regression/jbmc/nondet-static/My$PInner.class and b/jbmc/regression/jbmc/nondet-static/My$PInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My$PSInner.class b/jbmc/regression/jbmc/nondet-static/My$PSInner.class
index f3432fcb033..681100b4995 100644
Binary files a/jbmc/regression/jbmc/nondet-static/My$PSInner.class and b/jbmc/regression/jbmc/nondet-static/My$PSInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My$PrInner.class b/jbmc/regression/jbmc/nondet-static/My$PrInner.class
index 54c96ed1500..6da157fd288 100644
Binary files a/jbmc/regression/jbmc/nondet-static/My$PrInner.class and b/jbmc/regression/jbmc/nondet-static/My$PrInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My$PrSInner.class b/jbmc/regression/jbmc/nondet-static/My$PrSInner.class
index 2c9413cd7c3..844bce96d46 100644
Binary files a/jbmc/regression/jbmc/nondet-static/My$PrSInner.class and b/jbmc/regression/jbmc/nondet-static/My$PrSInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My.class b/jbmc/regression/jbmc/nondet-static/My.class
index df0cb67c701..c4830d093cf 100644
Binary files a/jbmc/regression/jbmc/nondet-static/My.class and b/jbmc/regression/jbmc/nondet-static/My.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My.java b/jbmc/regression/jbmc/nondet-static/My.java
index 6e8d6d86eef..04ffa03b5ee 100644
--- a/jbmc/regression/jbmc/nondet-static/My.java
+++ b/jbmc/regression/jbmc/nondet-static/My.java
@@ -96,143 +96,143 @@ private static class PrSInner {
     private static final Integer prf4 = new Integer(4);
   }
 
-  public int field;
   public My(int i) {
+
     String s = "bla";
-    field = i;
+
     if (p1 != 0)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 0; // this line can only be covered with nondet-static
     if (p2 != 1)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 1; // this line can only be covered with nondet-static
     if (p3 != 2)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 2; // this line can only be covered with nondet-static
     if (p4 != 3)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 3; // this line can only be covered with nondet-static
     if (!p5.equals(5))
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 4; // this line can only be covered with nondet-static
 
     if (pf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 5; // this line cannot be covered even with nondet-static
     if (pf2 != 2)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 6; // this line cannot be covered even with nondet-static
     if (pf3 != 3)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 7; // this line cannot be covered even with nondet-static
     if (!pf4.equals(4))
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 8; // this line cannot be covered even with nondet-static
 
     if (pr1 != 0)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 9; // this line can only be covered with nondet-static
     if (pr2 != 1)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 10; // this line can only be covered with nondet-static
     if (pr3 != 2)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 11; // this line can only be covered with nondet-static
     if (pr4 != 3)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 12; // this line can only be covered with nondet-static
     if (!pr5.equals(5))
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 13; // this line can only be covered with nondet-static
 
     if (prf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 14; // this line cannot be covered even with nondet-static
     if (prf2 != 2)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 15; // this line cannot be covered even with nondet-static
     if (prf3 != 3)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 16; // this line cannot be covered even with nondet-static
     if (!prf4.equals(4))
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 17; // this line cannot be covered even with nondet-static
 
     if (PInner.pf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 19; // this line cannot be covered even with nondet-static
 
     if (PInner.prf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 20; // this line cannot be covered even with nondet-static
 
     if (PSInner.p1 != 0)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 21; // this line can only be covered with nondet-static
     if (PSInner.p2 != 1)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 22; // this line can only be covered with nondet-static
     if (PSInner.p3 != 2)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 23; // this line can only be covered with nondet-static
     if (PSInner.p4 != 3)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 24; // this line can only be covered with nondet-static
     if (!PSInner.p5.equals(5))
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 25; // this line can only be covered with nondet-static
 
     if (PSInner.pf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 26; // this line cannot be covered even with nondet-static
     if (PSInner.pf2 != 2)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 27; // this line cannot be covered even with nondet-static
     if (PSInner.pf3 != 3)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 28; // this line cannot be covered even with nondet-static
     if (!PSInner.pf4.equals(4))
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 29; // this line cannot be covered even with nondet-static
 
     if (PSInner.pr1 != 0)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 30; // this line can only be covered with nondet-static
     if (PSInner.pr2 != 1)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 31; // this line can only be covered with nondet-static
     if (PSInner.pr3 != 2)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 32; // this line can only be covered with nondet-static
     if (PSInner.pr4 != 3)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 33; // this line can only be covered with nondet-static
     if (!PSInner.pr5.equals(5))
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 34; // this line can only be covered with nondet-static
 
     if (PSInner.prf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 35; // this line cannot be covered even with nondet-static
     if (PSInner.prf2 != 2)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 36; // this line cannot be covered even with nondet-static
     if (PSInner.prf3 != 3)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 37; // this line cannot be covered even with nondet-static
     if (!PSInner.prf4.equals(4))
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 38; // this line cannot be covered even with nondet-static
 
     if (PrInner.pf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 39; // this line cannot be covered even with nondet-static
 
     if (PrInner.prf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 40; // this line cannot be covered even with nondet-static
 
     if (PrSInner.p1 != 0)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 41; // this line can only be covered with nondet-static
     if (PrSInner.p2 != 1)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 42; // this line can only be covered with nondet-static
     if (PrSInner.p3 != 2)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 43; // this line can only be covered with nondet-static
     if (PrSInner.p4 != 3)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 44; // this line can only be covered with nondet-static
     if (!PrSInner.p5.equals(5))
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 45; // this line can only be covered with nondet-static
 
     if (PrSInner.pf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 46; // this line cannot be covered even with nondet-static
     if (PrSInner.pf2 != 2)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 47; // this line cannot be covered even with nondet-static
     if (PrSInner.pf3 != 3)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 48; // this line cannot be covered even with nondet-static
     if (!PrSInner.pf4.equals(4))
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 49; // this line cannot be covered even with nondet-static
 
     if (PrSInner.pr1 != 0)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 50; // this line can only be covered with nondet-static
     if (PrSInner.pr2 != 1)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 51; // this line can only be covered with nondet-static
     if (PrSInner.pr3 != 2)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 52; // this line can only be covered with nondet-static
     if (PrSInner.pr4 != 3)
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 53; // this line can only be covered with nondet-static
     if (!PrSInner.pr5.equals(5))
-      field = 108; // this line can only be covered with nondet-static
+      assert i == 54; // this line can only be covered with nondet-static
 
     if (PrSInner.prf1 != 1)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 55; // this line cannot be covered even with nondet-static
     if (PrSInner.prf2 != 2)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 56; // this line cannot be covered even with nondet-static
     if (PrSInner.prf3 != 3)
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 57; // this line cannot be covered even with nondet-static
     if (!PSInner.prf4.equals(4))
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 58; // this line cannot be covered even with nondet-static
 
     if (s != "bla")
-      field = 108; // this line cannot be covered even with nondet-static
+      assert i == 59; // this line cannot be covered even with nondet-static
   }
 }
diff --git a/jbmc/regression/jbmc/nondet-static/test.desc b/jbmc/regression/jbmc/nondet-static/test.desc
index 36b8fd59718..f401d5bfe06 100644
--- a/jbmc/regression/jbmc/nondet-static/test.desc
+++ b/jbmc/regression/jbmc/nondet-static/test.desc
@@ -1,57 +1,57 @@
 CORE symex-driven-lazy-loading-expected-failure
 My.class
---function "My.<init>" --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
-^EXIT=0$
+--function "My.<init>" --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^EXIT=10$
 ^SIGNAL=0$
-file My\.java line 104 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 106 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 108 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 110 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 112 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 117 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 119 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 121 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 124 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 126 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 128 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 130 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 132 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 137 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 139 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 141 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 150 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 152 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 154 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 156 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 158 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 163 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 165 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 167 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 170 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 172 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 174 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 176 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 178 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 183 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 185 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 187 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 196 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 198 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 200 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 202 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 204 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 209 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 211 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 213 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 216 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 218 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 220 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 222 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 224 function java::My\.\<init\>:\(I\)V.*SATISFIED$
-file My\.java line 229 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 231 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 233 function java::My\.\<init\>:\(I\)V.*FAILED$
-file My\.java line 236 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 104 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 106 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 108 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 110 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 112 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 117 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 119 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 121 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 124 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 126 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 128 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 130 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 132 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 137 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 139 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 141 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 150 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 152 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 154 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 156 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 158 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 163 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 165 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 167 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 170 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 172 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 174 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 176 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 178 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 183 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 185 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 187 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 196 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 198 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 200 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 202 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 204 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 209 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 211 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 213 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 216 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 218 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 220 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 222 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 224 function java::My\.\<init\>:\(I\)V.*FAILURE$
+file My\.java line 229 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 231 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 233 function java::My\.\<init\>:\(I\)V.*SUCCESS$
+file My\.java line 236 function java::My\.\<init\>:\(I\)V.*SUCCESS$
 --
 file My\.java line 115 function java::My\.\<init\>:\(I\)V
 file My\.java line 135 function java::My\.\<init\>:\(I\)V
diff --git a/jbmc/regression/jbmc/reachability-slice/A.class b/jbmc/regression/jbmc/reachability-slice/A.class
index 7f527e5fa9a..11dea827812 100644
Binary files a/jbmc/regression/jbmc/reachability-slice/A.class and b/jbmc/regression/jbmc/reachability-slice/A.class differ
diff --git a/jbmc/regression/jbmc/reachability-slice/A.java b/jbmc/regression/jbmc/reachability-slice/A.java
index 7680ebd172f..f0fe5bb037b 100644
--- a/jbmc/regression/jbmc/reachability-slice/A.java
+++ b/jbmc/regression/jbmc/reachability-slice/A.java
@@ -4,11 +4,14 @@ public void foo(int i ) {
       // We use integer constants that we grep for later in a goto program.
       int x = 1001 + i;
       if (i > 0) {
-        x = 1002 + i; // property "java::A.foo:(I)V.coverage.3", see https://github.com/diffblue/cbmc/pull/1943#discussion_r175367063 for a discusison.
+        x = 1002 + i;
         x = 1003 + i;
+        assert false;
       }
-      else
+      else {
         x = 1004 + i;
+        assert false;
+      }
       x = 1005 + i;  
     }
 }
diff --git a/jbmc/regression/jbmc/reachability-slice/test.desc b/jbmc/regression/jbmc/reachability-slice/test.desc
index c997bae2a05..0ddbc9d0505 100644
--- a/jbmc/regression/jbmc/reachability-slice/test.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test.desc
@@ -1,13 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
---reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
+--reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.1'
 = \(int\)\(short\)1001
---
+= \(int\)\(short\)1002
 = \(int\)\(short\)1003
+--
 = \(int\)\(short\)1004
 = \(int\)\(short\)1005
 --
-Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
-At the time of writing of this test, 1002 is removed.
-
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/jbmc/regression/jbmc/reachability-slice/test2.desc b/jbmc/regression/jbmc/reachability-slice/test2.desc
index 93b579d1b63..11c64768983 100644
--- a/jbmc/regression/jbmc/reachability-slice/test2.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test2.desc
@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
---reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
+--reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.2'
 = \(int\)\(short\)1001
+= \(int\)\(short\)1004
+--
 = \(int\)\(short\)1002
 = \(int\)\(short\)1003
 = \(int\)\(short\)1005
 --
-= \(int\)\(short\)1004
---
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/jbmc/regression/jbmc/reachability-slice/test3.desc b/jbmc/regression/jbmc/reachability-slice/test3.desc
index 7b10cf97e1a..4c7e8091dc8 100644
--- a/jbmc/regression/jbmc/reachability-slice/test3.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test3.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
---reachability-slice --show-goto-functions --cover location
+--reachability-slice --function A.foo --show-goto-functions
 = \(int\)\(short\)1001
 = \(int\)\(short\)1002
 = \(int\)\(short\)1003
diff --git a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
index 8bbea6300ec..defa750d6ab 100644
--- a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
+++ b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 VirtualFunctions.class
---lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function VirtualFunctions.check --show-goto-functions
+--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function VirtualFunctions.check --show-goto-functions
  \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$
  a \. VirtualFunctions\$A\.f:\(\)V\(\);$
  b \. VirtualFunctions\$B\.f:\(\)V\(\);$
diff --git a/jbmc/regression/jbmc/removed_virtual_functions/test.desc b/jbmc/regression/jbmc/removed_virtual_functions/test.desc
index cf36ec36380..632fb272be9 100644
--- a/jbmc/regression/jbmc/removed_virtual_functions/test.desc
+++ b/jbmc/regression/jbmc/removed_virtual_functions/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 ArrayListEquals.class
---lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions
+--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function ArrayListEquals.check2 --show-goto-functions
 e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc/stack_var12/test.desc b/jbmc/regression/jbmc/stack_var12/test.desc
index 27eaa97285e..158fcd8e452 100644
--- a/jbmc/regression/jbmc/stack_var12/test.desc
+++ b/jbmc/regression/jbmc/stack_var12/test.desc
@@ -1,9 +1,9 @@
 CORE
 stack_typecast.class
---cover location --function stack_typecast.f
-^EXIT=0$
+--function stack_typecast.f
+^EXIT=10$
 ^SIGNAL=0$
-covered \(100.0%\)
+^VERIFICATION FAILED$
 --
 --
 This tests that there is no invariant violation when modifying the values on the
diff --git a/jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class b/jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class
index e3dcef537a3..d69b188bf01 100644
Binary files a/jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class and b/jbmc/regression/jbmc/string_field_aliasing/Cart$Category.class differ
diff --git a/jbmc/regression/jbmc/string_field_aliasing/Cart$Product.class b/jbmc/regression/jbmc/string_field_aliasing/Cart$Product.class
index de058dc87d4..57f0ffb6fd8 100644
Binary files a/jbmc/regression/jbmc/string_field_aliasing/Cart$Product.class and b/jbmc/regression/jbmc/string_field_aliasing/Cart$Product.class differ
diff --git a/jbmc/regression/jbmc/string_field_aliasing/Cart.class b/jbmc/regression/jbmc/string_field_aliasing/Cart.class
index ec467604922..fafa6c123d2 100644
Binary files a/jbmc/regression/jbmc/string_field_aliasing/Cart.class and b/jbmc/regression/jbmc/string_field_aliasing/Cart.class differ
diff --git a/jbmc/regression/jbmc/string_field_aliasing/Cart.java b/jbmc/regression/jbmc/string_field_aliasing/Cart.java
index d14d35baafc..a499e1cd142 100644
--- a/jbmc/regression/jbmc/string_field_aliasing/Cart.java
+++ b/jbmc/regression/jbmc/string_field_aliasing/Cart.java
@@ -11,6 +11,8 @@ class Category {
 
     public boolean checkTax4(Product product, String s) {
         product.size="abc";
-        return s.startsWith(product.cat.name);
+        boolean result = s.startsWith(product.cat.name);
+	assert !result;
+	return result;
     }
 }
diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc
index 0666460000c..f3e41c0662f 100644
--- a/jbmc/regression/jbmc/string_field_aliasing/test.desc
+++ b/jbmc/regression/jbmc/string_field_aliasing/test.desc
@@ -1,13 +1,11 @@
 CORE
 Cart.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --cover location --java-max-vla-length 96 --refine-strings --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
-^EXIT=0$
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --java-max-vla-length 96 --refine-strings --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
+^EXIT=10$
 ^SIGNAL=0$
-checkTax4:.*: SATISFIED
+^VERIFICATION FAILED$
 --
-checkTax4:.*bytecode-index 8.*: FAILED
 dec_solve: current index set is empty, this should not happen
 --
 This checks that assigning to a field of an object (which generates a WITH expression in this case) doesn't result
-in conflating the String-typed and non-String-typed fields of the Cart class. When they are conflated we get
-warnings from the string solver and missing coverage.
+in conflating the String-typed and non-String-typed fields of the Cart class. When they are conflated we get warnings from the string solver.
diff --git a/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.class b/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.class
index 4238fc097d6..d81426ff313 100644
Binary files a/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.class and b/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.class differ
diff --git a/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.java b/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.java
index bfb5cdfeccc..8c8d8e5a402 100644
--- a/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.java
+++ b/jbmc/regression/jbmc/trace_class_identifier/TestGenTest.java
@@ -3,5 +3,6 @@ public class TestGenTest
   public void f()
   {
     int a = 4;
+    assert false;
   }
 }
diff --git a/jbmc/regression/jbmc/trace_class_identifier/test.desc b/jbmc/regression/jbmc/trace_class_identifier/test.desc
index 5514cd02ba0..6b9e42530fa 100644
--- a/jbmc/regression/jbmc/trace_class_identifier/test.desc
+++ b/jbmc/regression/jbmc/trace_class_identifier/test.desc
@@ -1,8 +1,8 @@
 CORE
 TestGenTest.class
---function TestGenTest.f --trace --cover location --json-ui
+--function TestGenTest.f --trace --json-ui
 "data": "java::TestGenTest",$
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring