diff --git a/regression/cbmc-cover/simple_assert/main.c b/regression/cbmc-cover/simple_assert/main.c
index 14c6fc0f682..705106bf433 100644
--- a/regression/cbmc-cover/simple_assert/main.c
+++ b/regression/cbmc-cover/simple_assert/main.c
@@ -1,9 +1,7 @@
-#include <assert.h>
-
 int main(int argc, char *argv[])
 {
   int x = 5;
-  assert(x == 5);
+  __CPROVER_assert(x == 5, "assertion x == 5");
 
   return 0;
 }
diff --git a/regression/cbmc-cover/simple_assert/test.desc b/regression/cbmc-cover/simple_assert/test.desc
index d3fac6c4c46..8a93d51f420 100644
--- a/regression/cbmc-cover/simple_assert/test.desc
+++ b/regression/cbmc-cover/simple_assert/test.desc
@@ -9,5 +9,3 @@ main.c
 ^warning: ignoring
 ^CONVERSION ERROR$
 ^\[main\.coverage\..\] .* function main block .*: FAILED$
---
-On Windows/Visual Studio, "assert" does not introduce any branching.
diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.c b/regression/cbmc-incr-oneloop/multiple-asserts/test.c
index b59f9ef2ad5..24d2d7563bc 100644
--- a/regression/cbmc-incr-oneloop/multiple-asserts/test.c
+++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.c
@@ -2,8 +2,8 @@ int main()
 {
   for(int i = 0; i < 10; ++i)
   {
-    assert(i != 5);
-    assert(i != 8);
+    __CPROVER_assert(i != 5, "assertion i != 5");
+    __CPROVER_assert(i != 8, "assertion i != 8");
   }
   return 0;
 }
diff --git a/regression/cbmc/Bool5/test.desc b/regression/cbmc/Bool5/test.desc
index 049b2be127c..80e137a91d2 100644
--- a/regression/cbmc/Bool5/test.desc
+++ b/regression/cbmc/Bool5/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 
-Generated 4 VCC\(s\), 0 remaining after simplification
+Generated [34] VCC\(s\), 0 remaining after simplification
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.c b/regression/cbmc/Quantifiers-not-exists/fixed.c
index 800571a3033..edc2c724271 100644
--- a/regression/cbmc/Quantifiers-not-exists/fixed.c
+++ b/regression/cbmc/Quantifiers-not-exists/fixed.c
@@ -10,33 +10,43 @@ int main()
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && a[i][j]<=10}) });
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) && b[i][j]>=1 && b[i][j]<=10}) });
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (!__CPROVER_exists{int j; (j>=0 && j<2) && (c[i][j]==0 || c[i][j]<=10)}) });
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
   // NOLINTNEXTLINE(whitespace/line_length)
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_forall{int j; (j>=0 && j<2) ==> d[i][j]>=1 && d[i][j]<=10}) });
   // clang-format on
 
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 
-  assert(a[0][0] > 10);
+  __CPROVER_assert(a[0][0] > 10, "assertion a[0][0] > 10");
 
-  assert((b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10));
-  assert((b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10));
+  __CPROVER_assert(
+    (b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10),
+    "assertion (b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10)");
+  __CPROVER_assert(
+    (b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10),
+    "assertion (b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)");
 
-  assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10);
+  __CPROVER_assert(
+    c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10,
+    "assertion (b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)");
 
-  assert(((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)));
-  assert(((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)));
+  __CPROVER_assert(
+    (d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10),
+    "assertion (d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)");
+  __CPROVER_assert(
+    (d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10),
+    "assertion (d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)");
 
   return 0;
 }
diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.desc b/regression/cbmc/Quantifiers-not-exists/fixed.desc
index 4e784a1b684..55c855af15f 100644
--- a/regression/cbmc/Quantifiers-not-exists/fixed.desc
+++ b/regression/cbmc/Quantifiers-not-exists/fixed.desc
@@ -2,12 +2,12 @@ CORE broken-z3-smt-backend
 fixed.c
 
 ^\*\* Results:$
-^\[main.assertion.5\] line 31 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.6\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.7\] line 34 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.8\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.9\] line 38 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.10\] line 39 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.5\] line 31 assertion a\[0\]\[0\] > 10: SUCCESS$
+^\[main.assertion.6\] line 33 .*: SUCCESS$
+^\[main.assertion.7\] line 36 .*: SUCCESS$
+^\[main.assertion.8\] line 40 .*: SUCCESS$
+^\[main.assertion.9\] line 44 .*: SUCCESS$
+^\[main.assertion.10\] line 47 .*: SUCCESS$
 ^\*\* 4 of 10 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
diff --git a/regression/cbmc/double_deref/double_deref.c b/regression/cbmc/double_deref/double_deref.c
index bc671f18b79..ece24937e37 100644
--- a/regression/cbmc/double_deref/double_deref.c
+++ b/regression/cbmc/double_deref/double_deref.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -12,5 +10,5 @@ int main(int argc, char **argv)
 
   pptr = (argc == 5 ? &ptr1 : &ptr2);
 
-  assert(**pptr == argc);
+  __CPROVER_assert(**pptr == argc, "assertion **pptr == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_single_alias.c b/regression/cbmc/double_deref/double_deref_single_alias.c
index 653446c256e..4c4d332957f 100644
--- a/regression/cbmc/double_deref/double_deref_single_alias.c
+++ b/regression/cbmc/double_deref/double_deref_single_alias.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -10,5 +8,5 @@ int main(int argc, char **argv)
 
   pptr = &ptr1;
 
-  assert(**pptr == argc);
+  __CPROVER_assert(**pptr == argc, "assertion **pptr == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_with_cast.c b/regression/cbmc/double_deref/double_deref_with_cast.c
index 6517156f83f..56c877455a4 100644
--- a/regression/cbmc/double_deref/double_deref_with_cast.c
+++ b/regression/cbmc/double_deref/double_deref_with_cast.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -12,5 +10,5 @@ int main(int argc, char **argv)
 
   pptr = (argc == 1 ? &ptr1 : &ptr2);
 
-  assert(*(int *)*pptr == argc);
+  __CPROVER_assert(*(int *)*pptr == argc, "assertion *(int *)*pptr == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_with_cast_single_alias.c b/regression/cbmc/double_deref/double_deref_with_cast_single_alias.c
index a7d9e9f00f2..3a2bdc2888f 100644
--- a/regression/cbmc/double_deref/double_deref_with_cast_single_alias.c
+++ b/regression/cbmc/double_deref/double_deref_with_cast_single_alias.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 int main(int argc, char **argv)
@@ -10,5 +8,5 @@ int main(int argc, char **argv)
 
   pptr = &ptr1;
 
-  assert(*(int *)*pptr == argc);
+  __CPROVER_assert(*(int *)*pptr == argc, "assertion *(int *)*pptr == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_with_member.c b/regression/cbmc/double_deref/double_deref_with_member.c
index fbebcc80b0d..99da33d65f7 100644
--- a/regression/cbmc/double_deref/double_deref_with_member.c
+++ b/regression/cbmc/double_deref/double_deref_with_member.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -18,5 +16,5 @@ int main(int argc, char **argv)
 
   cptr = (argc == 1 ? &container1 : &container2);
 
-  assert(*(cptr->iptr) == argc);
+  __CPROVER_assert(*(cptr->iptr) == argc, "assertion *(cptr->iptr) == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_with_member_single_alias.c b/regression/cbmc/double_deref/double_deref_with_member_single_alias.c
index c7ba385de08..b1045786b64 100644
--- a/regression/cbmc/double_deref/double_deref_with_member_single_alias.c
+++ b/regression/cbmc/double_deref/double_deref_with_member_single_alias.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -16,5 +14,5 @@ int main(int argc, char **argv)
 
   cptr = &container1;
 
-  assert(*(cptr->iptr) == argc);
+  __CPROVER_assert(*(cptr->iptr) == argc, "assertion *(cptr->iptr) == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c
index 62ff0738d1b..055721e0b48 100644
--- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c
+++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -18,5 +16,6 @@ int main(int argc, char **argv)
   new_ptrs[argc % 2] = iptr1;
   new_ptrs[1 - (argc % 2)] = iptr2;
 
-  assert(*(new_ptrs[argc % 2]) == argc);
+  __CPROVER_assert(
+    *(new_ptrs[argc % 2]) == argc, "assertion *(new_ptrs[argc % 2]) == argc");
 }
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c
index cf6646e4594..7187ee16b6d 100644
--- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c
+++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.c
@@ -1,5 +1,3 @@
-
-#include <assert.h>
 #include <stdlib.h>
 
 struct container
@@ -15,5 +13,6 @@ int main(int argc, char **argv)
 
   new_ptrs[argc % 2] = iptr1;
 
-  assert(*(new_ptrs[argc % 2]) == argc);
+  __CPROVER_assert(
+    *(new_ptrs[argc % 2]) == argc, "assertion *(new_ptrs[argc % 2]) == argc");
 }
diff --git a/regression/cbmc/json-interface1/main.c b/regression/cbmc/json-interface1/main.c
index 5fc3c2860bb..393698789fd 100644
--- a/regression/cbmc/json-interface1/main.c
+++ b/regression/cbmc/json-interface1/main.c
@@ -1,12 +1,10 @@
-#include <assert.h>
-
 void foo(int x)
 {
   for(int i = 0; i < 5; ++i)
   {
     if(x)
-      assert(0);
-    assert(0);
+      __CPROVER_assert(0, "assertion 0");
+    __CPROVER_assert(0, "assertion 0");
   }
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 }
diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc
index a15a7b20943..9ce2d4f907e 100644
--- a/regression/cbmc/json-interface1/test.desc
+++ b/regression/cbmc/json-interface1/test.desc
@@ -4,7 +4,7 @@ CORE
 activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
-Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
 \{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
 \{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
 VERIFICATION FAILED
diff --git a/regression/cbmc/multiple-goto-traces/main.c b/regression/cbmc/multiple-goto-traces/main.c
index 782c651393e..639f668c571 100644
--- a/regression/cbmc/multiple-goto-traces/main.c
+++ b/regression/cbmc/multiple-goto-traces/main.c
@@ -1,14 +1,12 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
-  assert(4 != argc);
+  __CPROVER_assert(4 != argc, "assertion 4 != argc");
   argc++;
   argc--;
-  assert(argc >= 0);
-  assert(argc != 4);
+  __CPROVER_assert(argc >= 0, "assertion argc >= 0");
+  __CPROVER_assert(argc != 4, "assertion argc != 4");
   argc++;
   argc--;
-  assert(argc + 1 != 5);
+  __CPROVER_assert(argc + 1 != 5, "assertion argc + 1 != 5");
   return 0;
 }
diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc
index 6a461a6a137..64427207060 100644
--- a/regression/cbmc/r_w_ok1/test.desc
+++ b/regression/cbmc/r_w_ok1/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
-^\*\* 2 of 12 failed
+^\*\* [12] of 12 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc/r_w_ok5/main.c b/regression/cbmc/r_w_ok5/main.c
index 1b4884e09bb..649943156ed 100644
--- a/regression/cbmc/r_w_ok5/main.c
+++ b/regression/cbmc/r_w_ok5/main.c
@@ -1,17 +1,16 @@
-#include <assert.h>
 #include <stdlib.h>
 
 void main()
 {
   char c[2];
-  assert(__CPROVER_r_ok(c, 2));
-  assert(!__CPROVER_r_ok(c, 2));
-  assert(__CPROVER_r_ok(c, 3));
-  assert(!__CPROVER_r_ok(c, 3));
+  __CPROVER_assert(__CPROVER_r_ok(c, 2), "assertion __CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(!__CPROVER_r_ok(c, 2), "assertion !__CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(__CPROVER_r_ok(c, 3), "assertion __CPROVER_r_ok(c, 3)");
+  __CPROVER_assert(!__CPROVER_r_ok(c, 3), "assertion !__CPROVER_r_ok(c, 3)");
 
   char *p = malloc(2);
-  assert(__CPROVER_r_ok(c, 2));
-  assert(!__CPROVER_r_ok(c, 2));
-  assert(__CPROVER_r_ok(p, 3));
-  assert(!__CPROVER_r_ok(p, 3));
+  __CPROVER_assert(__CPROVER_r_ok(c, 2), "assertion __CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(!__CPROVER_r_ok(c, 2), "assertion !__CPROVER_r_ok(c, 2)");
+  __CPROVER_assert(__CPROVER_r_ok(p, 3), "assertion __CPROVER_r_ok(p, 3)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 3), "assertion !__CPROVER_r_ok(p, 3)");
 }
diff --git a/regression/cbmc/r_w_ok6/main.c b/regression/cbmc/r_w_ok6/main.c
index a1c2855f011..4b41cfab154 100644
--- a/regression/cbmc/r_w_ok6/main.c
+++ b/regression/cbmc/r_w_ok6/main.c
@@ -1,4 +1,3 @@
-#include <assert.h>
 #include <stdlib.h>
 
 void main()
@@ -15,12 +14,12 @@ void main()
     p = malloc(3);
   }
 
-  assert(__CPROVER_r_ok(p, 2));
-  assert(!__CPROVER_r_ok(p, 2));
+  __CPROVER_assert(__CPROVER_r_ok(p, 2), "assertion __CPROVER_r_ok(p, 2)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 2), "assertion !__CPROVER_r_ok(p, 2)");
 
-  assert(__CPROVER_r_ok(p, 3));
-  assert(!__CPROVER_r_ok(p, 3));
+  __CPROVER_assert(__CPROVER_r_ok(p, 3), "assertion __CPROVER_r_ok(p, 3)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 3), "assertion !__CPROVER_r_ok(p, 3)");
 
-  assert(__CPROVER_r_ok(p, 4));
-  assert(!__CPROVER_r_ok(p, 4));
+  __CPROVER_assert(__CPROVER_r_ok(p, 4), "assertion __CPROVER_r_ok(p, 4)");
+  __CPROVER_assert(!__CPROVER_r_ok(p, 4), "assertion !__CPROVER_r_ok(p, 4)");
 }
diff --git a/regression/cbmc/reachability-slice-interproc/test.c b/regression/cbmc/reachability-slice-interproc/test.c
index f149e6f0976..b6aeed82199 100644
--- a/regression/cbmc/reachability-slice-interproc/test.c
+++ b/regression/cbmc/reachability-slice-interproc/test.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 // After a reachability slice based on the assertion in `target`, we should
 // retain both its possible callers (...may_call_target_1, ...may_call_target_2)
 // and their callees, but should be more precise concerning before_target and
@@ -22,7 +20,7 @@ void target()
   const char *local = "target_kept";
 
   before_target();
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
   after_target();
 }
 
diff --git a/regression/cbmc/xml-interface1/main.c b/regression/cbmc/xml-interface1/main.c
index 5fc3c2860bb..393698789fd 100644
--- a/regression/cbmc/xml-interface1/main.c
+++ b/regression/cbmc/xml-interface1/main.c
@@ -1,12 +1,10 @@
-#include <assert.h>
-
 void foo(int x)
 {
   for(int i = 0; i < 5; ++i)
   {
     if(x)
-      assert(0);
-    assert(0);
+      __CPROVER_assert(0, "assertion 0");
+    __CPROVER_assert(0, "assertion 0");
   }
-  assert(0);
+  __CPROVER_assert(0, "assertion 0");
 }
diff --git a/regression/cbmc/xml-interface1/test.desc b/regression/cbmc/xml-interface1/test.desc
index 8ef70fe541a..99c5025d16c 100644
--- a/regression/cbmc/xml-interface1/test.desc
+++ b/regression/cbmc/xml-interface1/test.desc
@@ -3,7 +3,7 @@ CORE
 < test.xml
 ^EXIT=10$
 ^SIGNAL=0$
-Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+Not unwinding loop foo\.0 iteration 3 file main\.c line 3 function foo thread 0
 <result property="foo\.assertion\.3" status="SUCCESS"/>
 <result property="foo\.assertion\.1" status="FAILURE">
 <goto_trace>
diff --git a/regression/goto-analyzer/command_line_01/main.c b/regression/goto-analyzer/command_line_01/main.c
index 87a99a5ab05..b589db7e0d9 100644
--- a/regression/goto-analyzer/command_line_01/main.c
+++ b/regression/goto-analyzer/command_line_01/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int f00(int x)
 {
-  assert(x != 0);
+  __CPROVER_assert(x != 0, "assertion x != 0");
   return 0;
 }
 
@@ -10,7 +8,7 @@ int main(int argc, char **argv)
 {
   int v = 0;
   v = f00(v);
-  assert(v != 0);
+  __CPROVER_assert(v != 0, "assertion v != 0");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/command_line_01/test.desc b/regression/goto-analyzer/command_line_01/test.desc
index df714eaa6c1..0f0e21c115d 100644
--- a/regression/goto-analyzer/command_line_01/test.desc
+++ b/regression/goto-analyzer/command_line_01/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --verify --recursive-interprocedural --ahistorical --constants --one-domain-per-history
-\[main.assertion.1\] line 13 assertion v != 0: FAILURE \(if reachable\)
-\[f00.assertion.1\] line 5 assertion x != 0: FAILURE \(if reachable\)
+\[main.assertion.1\] line 11 assertion v != 0: FAILURE \(if reachable\)
+\[f00.assertion.1\] line 3 assertion x != 0: FAILURE \(if reachable\)
 Summary: 0 pass, 2 fail if reachable, 0 unknown
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/command_line_02/main.c b/regression/goto-analyzer/command_line_02/main.c
index 87a99a5ab05..b589db7e0d9 100644
--- a/regression/goto-analyzer/command_line_02/main.c
+++ b/regression/goto-analyzer/command_line_02/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int f00(int x)
 {
-  assert(x != 0);
+  __CPROVER_assert(x != 0, "assertion x != 0");
   return 0;
 }
 
@@ -10,7 +8,7 @@ int main(int argc, char **argv)
 {
   int v = 0;
   v = f00(v);
-  assert(v != 0);
+  __CPROVER_assert(v != 0, "assertion v != 0");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/command_line_02/test.desc b/regression/goto-analyzer/command_line_02/test.desc
index 33b2024c496..1ae552f27e4 100644
--- a/regression/goto-analyzer/command_line_02/test.desc
+++ b/regression/goto-analyzer/command_line_02/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --verify --recursive-interprocedural --ahistorical --constants --one-domain-per-location
-\[main.assertion.1\] line 13 assertion v != 0: FAILURE \(if reachable\)
-\[f00.assertion.1\] line 5 assertion x != 0: FAILURE \(if reachable\)
+\[main.assertion.1\] line 11 assertion v != 0: FAILURE \(if reachable\)
+\[f00.assertion.1\] line 3 assertion x != 0: FAILURE \(if reachable\)
 Summary: 0 pass, 2 fail if reachable, 0 unknown
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/constant_propagation_18/main.c b/regression/goto-analyzer/constant_propagation_18/main.c
index 6a42c1b597f..b2c18d8281c 100644
--- a/regression/goto-analyzer/constant_propagation_18/main.c
+++ b/regression/goto-analyzer/constant_propagation_18/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
   int i = 1;
   int *p = &i;
-  assert(*p == 1);
+  __CPROVER_assert(*p == 1, "assertion *p == 1");
 }
diff --git a/regression/goto-analyzer/constant_propagation_18/test-vsd.desc b/regression/goto-analyzer/constant_propagation_18/test-vsd.desc
index 6d9845703b9..05de044e15a 100644
--- a/regression/goto-analyzer/constant_propagation_18/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_18/test-vsd.desc
@@ -3,6 +3,6 @@ main.c
 --variable-sensitivity --verify --vsd-pointers constants
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] line 7 assertion \*p == 1: SUCCESS$
+^\[main.assertion.1\] line 5 assertion \*p == 1: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc
index 3594e0cdc8f..7c845058b24 100644
--- a/regression/goto-analyzer/constant_propagation_18/test.desc
+++ b/regression/goto-analyzer/constant_propagation_18/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] line 7 assertion \*p == 1: SUCCESS$
+^\[main.assertion.1\] line 5 assertion \*p == 1: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_19/main.c b/regression/goto-analyzer/constant_propagation_19/main.c
index 10f765f1958..8cc99c08a1f 100644
--- a/regression/goto-analyzer/constant_propagation_19/main.c
+++ b/regression/goto-analyzer/constant_propagation_19/main.c
@@ -1,10 +1,8 @@
-#include <assert.h>
-
 int main()
 {
   int x;
   int *p = &x;
   *p = 42;
-  assert(x == 42);
+  __CPROVER_assert(x == 42, "assertion x == 42");
   return 0;
 }
diff --git a/regression/goto-analyzer/constant_propagation_19/test-vsd.desc b/regression/goto-analyzer/constant_propagation_19/test-vsd.desc
index ad68f7c6955..4b5da119668 100644
--- a/regression/goto-analyzer/constant_propagation_19/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_19/test-vsd.desc
@@ -3,6 +3,6 @@ main.c
 --variable-sensitivity --verify --vsd-pointers constants
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] line 8 assertion x == 42: SUCCESS$
+^\[main.assertion.1\] line 6 assertion x == 42: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_19/test.desc b/regression/goto-analyzer/constant_propagation_19/test.desc
index a331e26fe28..e05cc5201eb 100644
--- a/regression/goto-analyzer/constant_propagation_19/test.desc
+++ b/regression/goto-analyzer/constant_propagation_19/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] line 8 assertion x == 42: SUCCESS$
+^\[main.assertion.1\] line 6 assertion x == 42: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/main.c b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c
index f80f5f042d4..d32cad65a23 100644
--- a/regression/goto-analyzer/constant_propagation_floating_point_div/main.c
+++ b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c
@@ -1,9 +1,7 @@
-#include <assert.h>
-
 #define ROUND_F(x) ((int)((x) + 0.5f))
 int eight = ROUND_F(100.0f / 12.0f);
 
 int main()
 {
-  assert(eight == 8);
+  __CPROVER_assert(eight == 8, "assertion eight == 8");
 }
diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc
index ce2d5e9da12..ad45e5cfc98 100644
--- a/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc
+++ b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] line 8 assertion eight == 8: SUCCESS$
+^\[main.assertion.1\] line 6 assertion eight == 8: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c
index 6b1e90e3427..fd6c413b060 100644
--- a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c
+++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c
@@ -1,4 +1,3 @@
-#include <assert.h>
 #include <fenv.h>
 #include <stdio.h>
 
@@ -15,13 +14,18 @@ int main(void)
   // be greater or smaller than 0.1
 
   // definitely not smaller than -0.1
-  assert((1.0f / 10.0f) - f < -0.1f);
+  __CPROVER_assert(
+    (1.0f / 10.0f) - f < -0.1f, "assertion (1.0f / 10.0f) - f < -0.1f");
   // might be smaller than 0
-  assert((1.0f / 10.0f) - f < 0.0f);
+  __CPROVER_assert(
+    (1.0f / 10.0f) - f < 0.0f, "assertion (1.0f / 10.0f) - f < 0.0f");
   // definitely smaller or equal to 0
-  assert((1.0f / 10.0f) - f <= 0.0f);
+  __CPROVER_assert(
+    (1.0f / 10.0f) - f <= 0.0f, "assertion (1.0f / 10.0f) - f <= 0.0f");
   // might be greater or equal to 0
-  assert((1.0f / 10.0f) - f >= 0.0f);
+  __CPROVER_assert(
+    (1.0f / 10.0f) - f >= 0.0f, "assertion (1.0f / 10.0f) - f >= 0.0f");
   // definitely not greater than 0
-  assert((1.0f / 10.0f) - f > 0.0f);
+  __CPROVER_assert(
+    (1.0f / 10.0f) - f > 0.0f, "assertion (1.0f / 10.0f) - f > 0.0f");
 }
diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc
index 543a5cce4a3..1d5a3a1670a 100644
--- a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc
+++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc
@@ -3,10 +3,10 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.assertion.1\] line 18 assertion \(1.0f / 10.0f\) - f < -0.1f: FAILURE \(if reachable\)
+\[main.assertion.1\] line 17 assertion \(1.0f / 10.0f\) - f < -0.1f: FAILURE \(if reachable\)
 \[main.assertion.2\] line 20 assertion \(1.0f / 10.0f\) - f < 0.0f: UNKNOWN
-\[main.assertion.3\] line 22 assertion \(1.0f / 10.0f\) - f <= 0.0f: SUCCESS
-\[main.assertion.4\] line 24 assertion \(1.0f / 10.0f\) - f >= 0.0f: UNKNOWN
-\[main.assertion.5\] line 26 assertion \(1.0f / 10.0f\) - f > 0.0f: FAILURE \(if reachable\)
+\[main.assertion.3\] line 23 assertion \(1.0f / 10.0f\) - f <= 0.0f: SUCCESS
+\[main.assertion.4\] line 26 assertion \(1.0f / 10.0f\) - f >= 0.0f: UNKNOWN
+\[main.assertion.5\] line 29 assertion \(1.0f / 10.0f\) - f > 0.0f: FAILURE \(if reachable\)
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_two_way_1/main.c b/regression/goto-analyzer/constant_propagation_two_way_1/main.c
index f1b83128283..bfc40a689df 100644
--- a/regression/goto-analyzer/constant_propagation_two_way_1/main.c
+++ b/regression/goto-analyzer/constant_propagation_two_way_1/main.c
@@ -1,11 +1,9 @@
-#include <assert.h>
-
 int main()
 {
   int x;
   if(x == 0)
   {
-    assert(!x);
+    __CPROVER_assert(!x, "assertion !x");
   }
   return 0;
 }
diff --git a/regression/goto-analyzer/constant_propagation_two_way_1/test.desc b/regression/goto-analyzer/constant_propagation_two_way_1/test.desc
index 79e9746229d..454d63446c8 100644
--- a/regression/goto-analyzer/constant_propagation_two_way_1/test.desc
+++ b/regression/goto-analyzer/constant_propagation_two_way_1/test.desc
@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] line 8 assertion !x: SUCCESS$
+^\[main.assertion.1\] line 6 assertion !x: SUCCESS$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/context_sensitivity_02/main.c b/regression/goto-analyzer/context_sensitivity_02/main.c
index dda9c6cb6c6..a992372b93e 100644
--- a/regression/goto-analyzer/context_sensitivity_02/main.c
+++ b/regression/goto-analyzer/context_sensitivity_02/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int negate(int x)
 {
   return -x;
@@ -11,7 +9,7 @@ int main(int argc, char **argv)
   int nx = negate(x);
   int nnx = negate(nx);
 
-  assert(x == nnx);
+  __CPROVER_assert(x == nnx, "assertion x == nnx");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/context_sensitivity_04/main.c b/regression/goto-analyzer/context_sensitivity_04/main.c
index de771519594..2e3fd2f9b4c 100644
--- a/regression/goto-analyzer/context_sensitivity_04/main.c
+++ b/regression/goto-analyzer/context_sensitivity_04/main.c
@@ -1,10 +1,8 @@
-#include <assert.h>
-
 int step(int x)
 {
   if(x == 0)
   {
-    assert(x == 0);
+    __CPROVER_assert(x == 0, "assertion x == 0");
     return 0;
   }
   else
@@ -18,7 +16,7 @@ int main(int argc, char **argv)
   int orig = 20;
   int res = step(orig);
 
-  assert(res == 0);
+  __CPROVER_assert(res == 0, "assertion res == 0");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/context_sensitivity_05/main.c b/regression/goto-analyzer/context_sensitivity_05/main.c
index 5d774fa71cc..05a4c789298 100644
--- a/regression/goto-analyzer/context_sensitivity_05/main.c
+++ b/regression/goto-analyzer/context_sensitivity_05/main.c
@@ -1,37 +1,54 @@
-#include <assert.h>
-
 void f00(int x, int y)
 {
   if(x < 0)
   {
     // Unreachable in all traces if they are considered individually
-    assert(x < 0);
-    assert(1);
-    assert(0);
+    __CPROVER_assert(x < 0, "assertion x < 0");
+    __CPROVER_assert(1, "assertion 1");
+    __CPROVER_assert(0, "assertion 0");
   }
 
-  assert(x >= 0); // True in all traces
-  assert(x < 0);  // False in all traces
-  assert(x < 2);  // Split; true in some, false in others
+  __CPROVER_assert(x >= 0, "assertion x >= 0"); // True in all traces
+  __CPROVER_assert(x < 0, "assertion x < 0");   // False in all traces
+  __CPROVER_assert(
+    x < 2, "assertion x < 2"); // Split; true in some, false in others
 
-  assert((x <= 0) ? 1 : y);                  // True in some, unknown in others
-  assert((x <= 1) ? 0 : y);                  // False in some, unknown in others
-  assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+  __CPROVER_assert(
+    (x <= 0) ? 1 : y,
+    "assertion (x <= 0) ? 1 : y"); // True in some, unknown in others
+  __CPROVER_assert(
+    (x <= 1) ? 0 : y,
+    "assertion (x <= 1) ? 0 : y"); // False in some, unknown in others
+  __CPROVER_assert(
+    (x <= 2) ? ((x <= 3) ? 1 : 0) : y,
+    "assertion (x <= 2) ? ((x <= 3) ? 1 : 0) : y"); // A mix of all three
 
   if(x < 5)
   {
     // Not reachable in all traces
-    assert((x <= 0) ? 1 : y); // True in some, unknown in others
-    assert((x <= 1) ? 0 : y); // False in some, unknown in others
-    assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+    __CPROVER_assert(
+      (x <= 0) ? 1 : y,
+      "assertion (x <= 0) ? 1 : y"); // True in some, unknown in others
+    __CPROVER_assert(
+      (x <= 1) ? 0 : y,
+      "assertion (x <= 1) ? 0 : y"); // False in some, unknown in others
+    __CPROVER_assert(
+      (x <= 2) ? ((x <= 3) ? 1 : 0) : y,
+      "assertion (x <= 2) ? ((x <= 3) ? 1 : 0) : y"); // A mix of all three
   }
 
   if(x < 3)
   {
     // Not reachable in all traces
-    assert((x <= 0) ? 1 : y); // True in some, unknown in others
-    assert((x <= 1) ? 0 : y); // False in some, unknown in others
-    assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+    __CPROVER_assert(
+      (x <= 0) ? 1 : y,
+      "assertion (x <= 0) ? 1 : y"); // True in some, unknown in others
+    __CPROVER_assert(
+      (x <= 1) ? 0 : y,
+      "assertion (x <= 1) ? 0 : y"); // False in some, unknown in others
+    __CPROVER_assert(
+      (x <= 2) ? ((x <= 3) ? 1 : 0) : y,
+      "assertion (x <= 2) ? ((x <= 3) ? 1 : 0) : y"); // A mix of all three
   }
 }
 
diff --git a/regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c b/regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c
index 944a8eb8f9f..6dc37e6d77e 100644
--- a/regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c
+++ b/regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int fun(int other)
 {
   if(other > 0)
@@ -16,7 +14,7 @@ int fun(int other)
 int main(int argc, char *argv[])
 {
   int z = fun(0);
-  assert(
-    z ==
-    0); // Unknown as flow-insensitive fails to stop the recursive case being explored
+  __CPROVER_assert(
+    z == 0,
+    "assertion z == 0"); // Unknown as flow-insensitive fails to stop the recursive case being explored
 }
diff --git a/regression/goto-analyzer/flow-insensitive-if/main.c b/regression/goto-analyzer/flow-insensitive-if/main.c
index 59daa389188..7c2ae96ae9b 100644
--- a/regression/goto-analyzer/flow-insensitive-if/main.c
+++ b/regression/goto-analyzer/flow-insensitive-if/main.c
@@ -1,18 +1,16 @@
-#include <assert.h>
-
 int main(int argc, char *argv[])
 {
   int y = 1;
   int z;
   if(y)
   {
-    assert(y != 0);
+    __CPROVER_assert(y != 0, "assertion y != 0");
     z = 1;
   }
   else
   {
-    assert(y == 0);
+    __CPROVER_assert(y == 0, "assertion y == 0");
     z = 0;
   }
-  assert(z == 1);
+  __CPROVER_assert(z == 1, "assertion z == 1");
 }
diff --git a/regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c b/regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c
index 2ee5506b148..dde310ed11e 100644
--- a/regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c
+++ b/regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int fun(int other)
 {
   if(other > 0)
@@ -16,5 +14,7 @@ int fun(int other)
 int main(int argc, char *argv[])
 {
   int z = fun(0);
-  assert(z == 0); // Success because flow-sensitivity blocks the branch
+  __CPROVER_assert(
+    z == 0,
+    "assertion z == 0"); // Success because flow-sensitivity blocks the branch
 }
diff --git a/regression/goto-analyzer/flow-sensitive-if/main.c b/regression/goto-analyzer/flow-sensitive-if/main.c
index 59daa389188..7c2ae96ae9b 100644
--- a/regression/goto-analyzer/flow-sensitive-if/main.c
+++ b/regression/goto-analyzer/flow-sensitive-if/main.c
@@ -1,18 +1,16 @@
-#include <assert.h>
-
 int main(int argc, char *argv[])
 {
   int y = 1;
   int z;
   if(y)
   {
-    assert(y != 0);
+    __CPROVER_assert(y != 0, "assertion y != 0");
     z = 1;
   }
   else
   {
-    assert(y == 0);
+    __CPROVER_assert(y == 0, "assertion y == 0");
     z = 0;
   }
-  assert(z == 1);
+  __CPROVER_assert(z == 1, "assertion z == 1");
 }
diff --git a/regression/goto-analyzer/history-output/main.c b/regression/goto-analyzer/history-output/main.c
index 6f2fab362a4..5022bdd8549 100644
--- a/regression/goto-analyzer/history-output/main.c
+++ b/regression/goto-analyzer/history-output/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
   int nondet1;
@@ -22,7 +20,7 @@ int main(int argc, char **argv)
     // because x is non-deterministic
   }
 
-  assert(x);
+  __CPROVER_assert(x, "assertion x");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/intervals_simple-loops/main.c b/regression/goto-analyzer/intervals_simple-loops/main.c
index 2f6eba4184b..2d332465161 100644
--- a/regression/goto-analyzer/intervals_simple-loops/main.c
+++ b/regression/goto-analyzer/intervals_simple-loops/main.c
@@ -1,15 +1,14 @@
-#include <assert.h>
 const int g_N = 2;
 
 void main(void)
 {
   for(int i = 0; i < g_N; i++)
   {
-    assert(0);
+    __CPROVER_assert(0, "assertion 0");
   }
 
   for(int j = 4; j >= g_N; j--)
   {
-    assert(0);
+    __CPROVER_assert(0, "assertion 0");
   }
 }
diff --git a/regression/goto-analyzer/intervals_simple-loops/test.desc b/regression/goto-analyzer/intervals_simple-loops/test.desc
index d3c31abbef1..a09bf94466e 100644
--- a/regression/goto-analyzer/intervals_simple-loops/test.desc
+++ b/regression/goto-analyzer/intervals_simple-loops/test.desc
@@ -3,8 +3,8 @@ main.c
 --intervals
 ^EXIT=0$
 ^SIGNAL=0$
-\[main\.assertion\.1\] line 8 assertion 0: UNKNOWN
-\[main\.assertion\.2\] line 13 assertion 0: UNKNOWN
+\[main\.assertion\.1\] line 7 assertion 0: UNKNOWN
+\[main\.assertion\.2\] line 12 assertion 0: UNKNOWN
 --
 --
 Test comparision between two symbols does not mark the
diff --git a/regression/goto-analyzer/local_control_flow_history_01/main.c b/regression/goto-analyzer/local_control_flow_history_01/main.c
index 69478446b48..33fe3a69c1b 100644
--- a/regression/goto-analyzer/local_control_flow_history_01/main.c
+++ b/regression/goto-analyzer/local_control_flow_history_01/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
   int branch;
@@ -15,7 +13,7 @@ int main(int argc, char **argv)
   }
 
   // Merging a constant domain here will make this unprovable
-  assert(x != 0);
+  __CPROVER_assert(x != 0, "assertion x != 0");
 
   // Some subtle points here...
   // The history tracks paths, it is up to the domain to track the
@@ -30,11 +28,11 @@ int main(int argc, char **argv)
   // one with branch == 0, x == 1.
   if(branch)
   {
-    assert(x == 1);
+    __CPROVER_assert(x == 1, "assertion x == 1");
   }
   else
   {
-    assert(x == -1);
+    __CPROVER_assert(x == -1, "assertion x == -1");
   }
 
   // Working around the domain issues...
@@ -49,7 +47,7 @@ int main(int argc, char **argv)
   }
 
   // Should be true in all 3 paths
-  assert(x == 0);
+  __CPROVER_assert(x == 0, "assertion x == 0");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/local_control_flow_history_02/main.c b/regression/goto-analyzer/local_control_flow_history_02/main.c
index e245deaeba7..c68f04bc314 100644
--- a/regression/goto-analyzer/local_control_flow_history_02/main.c
+++ b/regression/goto-analyzer/local_control_flow_history_02/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
   int branching_array[5];
@@ -10,21 +8,21 @@ int main(int argc, char **argv)
     ++x;
   }
   // Two paths...
-  assert(x > 0);
+  __CPROVER_assert(x > 0, "assertion x > 0");
 
   if(branching_array[1])
   {
     ++x;
   }
   // Four paths...
-  assert(x > 0);
+  __CPROVER_assert(x > 0, "assertion x > 0");
 
   if(branching_array[2])
   {
     ++x;
   }
   // Eight paths...
-  assert(x > 0);
+  __CPROVER_assert(x > 0, "assertion x > 0");
 
   if(branching_array[3])
   {
@@ -32,7 +30,7 @@ int main(int argc, char **argv)
   }
   // Paths merge so there will be some paths that will set x to \top
   // and so this will be flagged as unknown
-  assert(x > 0);
+  __CPROVER_assert(x > 0, "assertion x > 0");
   // In principle it would be possible to merge paths in such a way
   // that the those with similar domains are merged and this would be
   // able to be proved.  The local_control_flow_history code doesn't
diff --git a/regression/goto-analyzer/local_control_flow_history_03/main.c b/regression/goto-analyzer/local_control_flow_history_03/main.c
index 7f81bafaaa0..548ab3884c6 100644
--- a/regression/goto-analyzer/local_control_flow_history_03/main.c
+++ b/regression/goto-analyzer/local_control_flow_history_03/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
   int total = 0;
@@ -11,7 +9,8 @@ int main(int argc, char **argv)
     total += i;
   }
 
-  assert(total == (n * (n - 1) / 2));
+  __CPROVER_assert(
+    total == (n * (n - 1) / 2), "assertion total == (n * (n - 1) / 2)");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/local_control_flow_history_04/main.c b/regression/goto-analyzer/local_control_flow_history_04/main.c
index 6109908bd2f..e4e048065f8 100644
--- a/regression/goto-analyzer/local_control_flow_history_04/main.c
+++ b/regression/goto-analyzer/local_control_flow_history_04/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
   int total;
@@ -14,7 +12,8 @@ int main(int argc, char **argv)
   }
 
   // Unknown due to the limit on unwindings
-  assert(total == (n * (n - 1) / 2));
+  __CPROVER_assert(
+    total == (n * (n - 1) / 2), "assertion total == (n * (n - 1) / 2)");
 
   // Condense down to one path...
 
@@ -26,7 +25,8 @@ int main(int argc, char **argv)
   }
 
   // Creates a merge path but only one user of it
-  assert(total == (n * (n - 1) / 2));
+  __CPROVER_assert(
+    total == (n * (n - 1) / 2), "assertion total == (n * (n - 1) / 2)");
 
   total = 0;
   n = 32;
@@ -36,7 +36,8 @@ int main(int argc, char **argv)
   }
 
   // Provable
-  assert(total == (n * (n - 1) / 2));
+  __CPROVER_assert(
+    total == (n * (n - 1) / 2), "assertion total == (n * (n - 1) / 2)");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/local_control_flow_history_05/main.c b/regression/goto-analyzer/local_control_flow_history_05/main.c
index 320370adfd8..0a3997c53bc 100644
--- a/regression/goto-analyzer/local_control_flow_history_05/main.c
+++ b/regression/goto-analyzer/local_control_flow_history_05/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(int argc, char **argv)
 {
   int total;
@@ -17,7 +15,8 @@ int main(int argc, char **argv)
     }
   }
 
-  assert(total <= (n * (n - 1) / 2));
+  __CPROVER_assert(
+    total <= (n * (n - 1) / 2), "assertion total <= (n * (n - 1) / 2)");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/local_control_flow_history_06/main.c b/regression/goto-analyzer/local_control_flow_history_06/main.c
index 622e948cd30..1dce554e4f4 100644
--- a/regression/goto-analyzer/local_control_flow_history_06/main.c
+++ b/regression/goto-analyzer/local_control_flow_history_06/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 #define CODE_BLOCK                                                             \
   int i;                                                                       \
   float flotal = 0;                                                            \
@@ -7,7 +5,8 @@
   {                                                                            \
     flotal += i;                                                               \
   }                                                                            \
-  assert(flotal == (n * (n - 1) / 2))
+  __CPROVER_assert(                                                            \
+    flotal == (n * (n - 1) / 2), "assertion flotal == (n * (n - 1) / 2)")
 
 void do_the_loop(int n)
 {
diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c b/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c
index e501f842f30..7be16a32ad6 100644
--- a/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c
+++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main()
 {
   int unknown;
@@ -12,5 +10,5 @@ int main()
 
   int q = *p;
 
-  assert(q == a);
+  __CPROVER_assert(q == a, "assertion q == a");
 }
diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc
index f688ea2ab0f..623ad50b42b 100644
--- a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc
+++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants
-^\[main.assertion.1\] line 15 assertion q == a: SUCCESS
+^\[main.assertion.1\] line 13 assertion q == a: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc
index 4be05332a55..10064f59dd7 100644
--- a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc
+++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom
-^\[main.assertion.1\] line 15 assertion q == a: UNKNOWN
+^\[main.assertion.1\] line 13 assertion q == a: UNKNOWN
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc
index 1468aca72f3..78f4d2dd172 100644
--- a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc
+++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set
-^\[main.assertion.1\] line 15 assertion q == a: SUCCESS
+^\[main.assertion.1\] line 13 assertion q == a: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-dereference/main.c b/regression/goto-analyzer/pointer-dereference/main.c
index ea7b7207ec2..ebc3d065373 100644
--- a/regression/goto-analyzer/pointer-dereference/main.c
+++ b/regression/goto-analyzer/pointer-dereference/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main()
 {
   int a = 10;
@@ -7,5 +5,5 @@ int main()
 
   int q = *p;
 
-  assert(q == a);
+  __CPROVER_assert(q == a, "assertion q == a");
 }
diff --git a/regression/goto-analyzer/pointer-dereference/test-constants.desc b/regression/goto-analyzer/pointer-dereference/test-constants.desc
index 9c6c0f0b7fa..b834fd4ee73 100644
--- a/regression/goto-analyzer/pointer-dereference/test-constants.desc
+++ b/regression/goto-analyzer/pointer-dereference/test-constants.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-pointers constants
-^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
+^\[main.assertion.1\] line 8 assertion q == a: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc b/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc
index 8c498fb94f7..08cc92d06e6 100644
--- a/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc
+++ b/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-pointers top-bottom
-^\[main.assertion.1\] line 10 assertion q == a: UNKNOWN
+^\[main.assertion.1\] line 8 assertion q == a: UNKNOWN
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-dereference/test-value-sets.desc b/regression/goto-analyzer/pointer-dereference/test-value-sets.desc
index 5a2d3ecb552..12a22c3e0c0 100644
--- a/regression/goto-analyzer/pointer-dereference/test-value-sets.desc
+++ b/regression/goto-analyzer/pointer-dereference/test-value-sets.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-pointers value-set
-^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
+^\[main.assertion.1\] line 8 assertion q == a: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/main.c b/regression/goto-analyzer/pointer-write-through-indeterminate/main.c
index 3e983a025ec..ae7c6fa7e88 100644
--- a/regression/goto-analyzer/pointer-write-through-indeterminate/main.c
+++ b/regression/goto-analyzer/pointer-write-through-indeterminate/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main()
 {
   int unknown;
@@ -13,5 +11,5 @@ int main()
     *p = 15;
   }
 
-  assert(*p == b);
+  __CPROVER_assert(*p == b, "assertion *p == b");
 }
diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc
index 5f6414cd927..824b84bbcd0 100644
--- a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc
+++ b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants
-^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS
+^\[main.assertion.1\] line 14 assertion \*p == b: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc
index fc850b8e590..9b55799ee6a 100644
--- a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc
+++ b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom
-^\[main.assertion.1\] line 16 assertion \*p == b: UNKNOWN
+^\[main.assertion.1\] line 14 assertion \*p == b: UNKNOWN
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc
index 77ae5116c1d..38ad1af7d41 100644
--- a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc
+++ b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set
-^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS
+^\[main.assertion.1\] line 14 assertion \*p == b: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-write-through/main.c b/regression/goto-analyzer/pointer-write-through/main.c
index 6a5cc63dca0..f3016e4be86 100644
--- a/regression/goto-analyzer/pointer-write-through/main.c
+++ b/regression/goto-analyzer/pointer-write-through/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main()
 {
   int a = 10;
@@ -7,5 +5,5 @@ int main()
 
   *p = 15;
 
-  assert(a == 15);
+  __CPROVER_assert(a == 15, "assertion a == 15");
 }
diff --git a/regression/goto-analyzer/pointer-write-through/test-constants.desc b/regression/goto-analyzer/pointer-write-through/test-constants.desc
index bd09812d2e2..d34ad434a4f 100644
--- a/regression/goto-analyzer/pointer-write-through/test-constants.desc
+++ b/regression/goto-analyzer/pointer-write-through/test-constants.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-pointers constants
-^\[main.assertion.1\] line 10 assertion a == 15: SUCCESS
+^\[main.assertion.1\] line 8 assertion a == 15: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc b/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc
index 7d2abb2834f..f012b506e57 100644
--- a/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc
+++ b/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-pointers top-bottom
-^\[main.assertion.1\] line 10 assertion a == 15: UNKNOWN
+^\[main.assertion.1\] line 8 assertion a == 15: UNKNOWN
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/pointer-write-through/test-value-sets.desc b/regression/goto-analyzer/pointer-write-through/test-value-sets.desc
index 32f0f02564f..f6df4ff07cd 100644
--- a/regression/goto-analyzer/pointer-write-through/test-value-sets.desc
+++ b/regression/goto-analyzer/pointer-write-through/test-value-sets.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --verify --variable-sensitivity --vsd-pointers value-set
-^\[main.assertion.1\] line 10 assertion a == 15: SUCCESS
+^\[main.assertion.1\] line 8 assertion a == 15: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/sensitivity-function-call-array/main.c b/regression/goto-analyzer/sensitivity-function-call-array/main.c
index 3631bdd8fa8..c6036e64574 100644
--- a/regression/goto-analyzer/sensitivity-function-call-array/main.c
+++ b/regression/goto-analyzer/sensitivity-function-call-array/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int *bar(int *arr_unmodified, int *arr_modified);
 
 int main()
@@ -9,24 +7,24 @@ int main()
   int *p2arr = arr_x;
 
   p2arr = bar(arr_x, arr_y);
-  assert(*arr_y == 2);
-  // assert(arr_y[1]==3);
+  __CPROVER_assert(*arr_y == 2, "assertion *arr_y == 2");
+  // __CPROVER_assert(arr_y[1]==3, "assertion arr_y[1]==3");
 
-  assert(p2arr == arr_y);
-  assert(*p2arr == 2);
-  // assert(p2arr[1]==3);
+  __CPROVER_assert(p2arr == arr_y, "assertion p2arr == arr_y");
+  __CPROVER_assert(*p2arr == 2, "assertion *p2arr == 2");
+  // __CPROVER_assert(p2arr[1]==3, "assertion p2arr[1]==3");
 }
 
 int *bar(int *arr_unmodified, int *arr_modified)
 {
-  assert(*arr_unmodified == 1);
-  // assert(arr_unmodified[1]==2);
+  __CPROVER_assert(*arr_unmodified == 1, "assertion *arr_unmodified == 1");
+  // __CPROVER_assert(arr_unmodified[1]==2, "assertion arr_unmodified[1]==2");
 
   (*arr_modified) += 1;
   // arr_modified[1] = 3;
 
-  assert(*arr_modified == 2);
-  // assert(arr_modified[1]==3);
+  __CPROVER_assert(*arr_modified == 2, "assertion *arr_modified == 2");
+  // __CPROVER_assert(arr_modified[1]==3, "assertion arr_modified[1]==3");
 
   return arr_modified;
 }
diff --git a/regression/goto-analyzer/sensitivity-function-call-opaque/main.c b/regression/goto-analyzer/sensitivity-function-call-opaque/main.c
index aed3b161f1d..d8eb24e270c 100644
--- a/regression/goto-analyzer/sensitivity-function-call-opaque/main.c
+++ b/regression/goto-analyzer/sensitivity-function-call-opaque/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int global_value;
 
 int opaque(int other, int *side_effect);
@@ -13,12 +11,16 @@ int main()
 
   int z = bar(x + 1, &y);
 
-  assert(x == 3); // Success
-  assert(y == 4); // Unknown - the opaque function could have modified it
-  assert(z == 0); // Unknown - the opaque function could have returned anything
-  assert(
-    global_value ==
-    4); // Unknown - the opaque function could have modified this
+  __CPROVER_assert(x == 3, "assertion x == 3"); // Success
+  __CPROVER_assert(
+    y == 4,
+    "assertion y == 4"); // Unknown - the opaque function could have modified it
+  __CPROVER_assert(
+    z == 0,
+    "assertion z == 0"); // Unknown - the opaque function could have returned anything
+  __CPROVER_assert(
+    global_value == 4,
+    "assertion global_value == 4"); // Unknown - the opaque function could have modified this
 
   return 0;
 }
diff --git a/regression/goto-analyzer/sensitivity-function-call-pointer/main.c b/regression/goto-analyzer/sensitivity-function-call-pointer/main.c
index 6774abfa266..09e0ac60fc5 100644
--- a/regression/goto-analyzer/sensitivity-function-call-pointer/main.c
+++ b/regression/goto-analyzer/sensitivity-function-call-pointer/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int *bar(int *unmodified, int *modifed);
 
 int main()
@@ -8,18 +6,18 @@ int main()
   int y = 4;
   int *p2x = &x;
   p2x = bar(&x, &y);
-  assert(y == 5);
-  assert(p2x == &y);
-  assert(*p2x == 5);
+  __CPROVER_assert(y == 5, "assertion y == 5");
+  __CPROVER_assert(p2x == &y, "assertion p2x == &y");
+  __CPROVER_assert(*p2x == 5, "assertion *p2x == 5");
 }
 
 int *bar(int *unmodified, int *modifed)
 {
-  assert(*unmodified == 3);
+  __CPROVER_assert(*unmodified == 3, "assertion *unmodified == 3");
 
   (*modifed) += 1;
 
-  assert(*modifed == 5);
+  __CPROVER_assert(*modifed == 5, "assertion *modifed == 5");
 
   return modifed;
 }
diff --git a/regression/goto-analyzer/sensitivity-function-call-primitive/main.c b/regression/goto-analyzer/sensitivity-function-call-primitive/main.c
index 047f6ad44a5..3e5b39c5032 100644
--- a/regression/goto-analyzer/sensitivity-function-call-primitive/main.c
+++ b/regression/goto-analyzer/sensitivity-function-call-primitive/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int bar(int other)
 {
-  assert(other == 4);
+  __CPROVER_assert(other == 4, "assertion other == 4");
   return other + 1;
 }
 
@@ -10,5 +8,5 @@ int main()
 {
   int x = 3;
   int y = bar(x + 1);
-  assert(y == 5);
+  __CPROVER_assert(y == 5, "assertion y == 5");
 }
diff --git a/regression/goto-analyzer/sensitivity-function-call-recursive/main.c b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c
index 939fb0ab2e6..06ea41e90fa 100644
--- a/regression/goto-analyzer/sensitivity-function-call-recursive/main.c
+++ b/regression/goto-analyzer/sensitivity-function-call-recursive/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int bar(int other)
 {
   if(other > 0)
@@ -43,14 +41,17 @@ int main()
 {
   int x=3;
   int y=bar(x+1);
-  assert(y==4); // Unknown in the constants domain
+  __CPROVER_assert(y == 4, "assertion y==4"); // Unknown in the constants domain
 
   int y2 = bar(0);
-  assert(y2==0); // Unknown since we are not sensitive to call domain
+  __CPROVER_assert(
+    y2 == 0,
+    "assertion y2==0"); // Unknown since we are not sensitive to call domain
 
   int z = bar_clean(0);
-  assert(z==0); // Unknown as the function has parameter as top
+  __CPROVER_assert(
+    z == 0, "assertion z==0"); // Unknown as the function has parameter as top
 
   int w = fun(5, 18);
-  assert(w==18);
+  __CPROVER_assert(w == 18, "assertion w==18");
 }
diff --git a/regression/goto-analyzer/sensitivity-function-call-varargs/main.c b/regression/goto-analyzer/sensitivity-function-call-varargs/main.c
index 3aae33b7b0d..94a7ec79727 100644
--- a/regression/goto-analyzer/sensitivity-function-call-varargs/main.c
+++ b/regression/goto-analyzer/sensitivity-function-call-varargs/main.c
@@ -1,4 +1,3 @@
-#include <assert.h>
 #include <stdarg.h>
 
 int bar(int size, ...)
@@ -19,8 +18,8 @@ int bar(int size, ...)
 int main()
 {
   int y = bar(4, 1, 2, 2, 1);
-  assert(y == 6);
+  __CPROVER_assert(y == 6, "assertion y == 6");
 
   int z = bar(0);
-  assert(z == 0);
+  __CPROVER_assert(z == 0, "assertion z == 0");
 }
diff --git a/regression/goto-analyzer/value-set-simple/main.c b/regression/goto-analyzer/value-set-simple/main.c
index ed3f58f2319..34abe450d35 100644
--- a/regression/goto-analyzer/value-set-simple/main.c
+++ b/regression/goto-analyzer/value-set-simple/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int global_int = 0;
 int global_int_show = 0;
 
@@ -13,10 +11,12 @@ int main(void)
     global_int = 2;
   global_int_show = global_int;
 
-  assert(global_int == 2);
-  assert(global_int == 1 || global_int == 2);
-  assert(global_int > 0);
-  assert(global_int > 3);
+  __CPROVER_assert(global_int == 2, "assertion global_int == 2");
+  __CPROVER_assert(
+    global_int == 1 || global_int == 2,
+    "assertion global_int == 1 || global_int == 2");
+  __CPROVER_assert(global_int > 0, "assertion global_int > 0");
+  __CPROVER_assert(global_int > 3, "assertion global_int > 3");
 
   double local_double;
 
@@ -26,10 +26,12 @@ int main(void)
     local_double = 2.0;
   double local_double_show = local_double;
 
-  assert(local_double == 2.0);
-  assert(local_double == 1.0 || local_double == 2.0);
-  assert(local_double > 0.0);
-  assert(local_double > 3.0);
+  __CPROVER_assert(local_double == 2.0, "assertion local_double == 2.0");
+  __CPROVER_assert(
+    local_double == 1.0 || local_double == 2.0,
+    "assertion local_double == 1.0 || local_double == 2.0");
+  __CPROVER_assert(local_double > 0.0, "assertion local_double > 0.0");
+  __CPROVER_assert(local_double > 3.0, "assertion local_double > 3.0");
 
   double d1 = 1.0;
   double d2 = 2.0;
@@ -41,10 +43,15 @@ int main(void)
     local_double_ptr = &d2;
   double *local_double_ptr_show = local_double_ptr;
 
-  assert(local_double_ptr == &d2);
-  assert(local_double_ptr == &d1 || local_double == &d2);
-  assert(*local_double_ptr > 0.0);
-  assert(*local_double_ptr > 3.0);
+  __CPROVER_assert(
+    local_double_ptr == &d2, "assertion local_double_ptr == &d2");
+  __CPROVER_assert(
+    local_double_ptr == &d1 || local_double == &d2,
+    "assertion local_double_ptr == &d1 || local_double == &d2");
+  __CPROVER_assert(
+    *local_double_ptr > 0.0, "assertion *local_double_ptr > 0.0");
+  __CPROVER_assert(
+    *local_double_ptr > 3.0, "assertion *local_double_ptr > 3.0");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/value-set-structs/main.c b/regression/goto-analyzer/value-set-structs/main.c
index 422534487e2..6f8a158ea04 100644
--- a/regression/goto-analyzer/value-set-structs/main.c
+++ b/regression/goto-analyzer/value-set-structs/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 struct my_struct
 {
   int i;
@@ -31,16 +29,19 @@ int main(void)
 
   struct my_struct s_show = s;
 
-  assert(s.i == 0);
+  __CPROVER_assert(s.i == 0, "assertion s.i == 0");
 
-  assert(s.d == 1.0);
-  assert(s.d == 1.0 || s.d == 2.0);
-  assert(s.d > 0.0);
-  assert(s.d > 10.0);
+  __CPROVER_assert(s.d == 1.0, "assertion s.d == 1.0");
+  __CPROVER_assert(
+    s.d == 1.0 || s.d == 2.0, "assertion s.d == 1.0 || s.d == 2.0");
+  __CPROVER_assert(s.d > 0.0, "assertion s.d > 0.0");
+  __CPROVER_assert(s.d > 10.0, "assertion s.d > 10.0");
 
-  assert(s.str[0] == 'x');
-  assert(s.str[0] == 'x' || s.str[0] == 'y');
-  assert(s.str[1] == '\n');
+  __CPROVER_assert(s.str[0] == 'x', "assertion s.str[0] == 'x'");
+  __CPROVER_assert(
+    s.str[0] == 'x' || s.str[0] == 'y',
+    "assertion s.str[0] == 'x' || s.str[0] == 'y'");
+  __CPROVER_assert(s.str[1] == '\n', "assertion s.str[1] == '\n'");
 
   struct my_struct t = {1, 3.0, {'z', '\n'}};
   struct my_struct u;
@@ -52,16 +53,20 @@ int main(void)
 
   struct my_struct u_show = u;
 
-  assert(u.i == 1);
+  __CPROVER_assert(u.i == 1, "assertion u.i == 1");
 
-  assert(u.d == 3.0);
-  assert(u.d == 1.0 || u.d == 2.0 || u.d == 3.0);
-  assert(u.d > 0.0);
-  assert(u.d > 10.0);
+  __CPROVER_assert(u.d == 3.0, "assertion u.d == 3.0");
+  __CPROVER_assert(
+    u.d == 1.0 || u.d == 2.0 || u.d == 3.0,
+    "assertion u.d == 1.0 || u.d == 2.0 || u.d == 3.0");
+  __CPROVER_assert(u.d > 0.0, "assertion u.d > 0.0");
+  __CPROVER_assert(u.d > 10.0, "assertion u.d > 10.0");
 
-  assert(u.str[0] == 'z');
-  assert(u.str[0] == 'x' || u.str[0] == 'y' || u.str[0] == 'z');
-  assert(u.str[1] == '\n');
+  __CPROVER_assert(u.str[0] == 'z', "assertion u.str[0] == 'z'");
+  __CPROVER_assert(
+    u.str[0] == 'x' || u.str[0] == 'y' || u.str[0] == 'z',
+    "assertion u.str[0] == 'x' || u.str[0] == 'y' || u.str[0] == 'z'");
+  __CPROVER_assert(u.str[1] == '\n', "assertion u.str[1] == '\n'");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/main.c b/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/main.c
index 60fa538c805..78ca3ec8da5 100644
--- a/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/main.c
+++ b/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int main(void)
 {
   const float one = 1.0f;
@@ -9,7 +7,7 @@ int main(void)
   float big_0_1 = one / 10.0f;
   __CPROVER_rounding_mode = 1; // round to -∞
   float small_0_1 = one / 10.0f;
-  assert(small_0_1 < big_0_1);
+  __CPROVER_assert(small_0_1 < big_0_1, "assertion small_0_1 < big_0_1");
 
   // Check that exact operations still work with unknown rounding mode
   int some_condition;
@@ -21,7 +19,7 @@ int main(void)
 
   // regardless of rounding mode,
   // 1/10 is definitely smaller than 0.2
-  assert(one / 10.0f < 0.2f);
+  __CPROVER_assert(one / 10.0f < 0.2f, "assertion one / 10.0f < 0.2f");
 
   // This is unknown because
   // we don't know the value of one_tenth_ish
@@ -30,12 +28,12 @@ int main(void)
   // to know the exact value of one/10.0f, just
   // that it is less than 0.2f
   float one_tenth_ish = one / 10.0f;
-  assert(one_tenth_ish < 0.2f);
+  __CPROVER_assert(one_tenth_ish < 0.2f, "assertion one_tenth_ish < 0.2f");
 
   // regardless of rounding mode,
   // 10/5 is still 2
   float five = 5.0f;
-  assert(10.0f / five == 2.0f);
+  __CPROVER_assert(10.0f / five == 2.0f, "assertion 10.0f / five == 2.0f");
 
   return 0;
 }
diff --git a/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/test.desc b/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/test.desc
index a6456a135d5..07117338268 100644
--- a/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-floating-point-simplification/test.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion\.1\] line 12 assertion small_0_1 < big_0_1: SUCCESS
-^\[main.assertion\.2\] line 24 assertion one / 10.0f < 0.2f: SUCCESS
-^\[main.assertion\.3\] line 33 assertion one_tenth_ish < 0.2f: UNKNOWN
-^\[main.assertion\.4\] line 38 assertion 10.0f / five == 2.0f: SUCCESS
+^\[main.assertion\.1\] line 10 assertion small_0_1 < big_0_1: SUCCESS
+^\[main.assertion\.2\] line 22 assertion one / 10.0f < 0.2f: SUCCESS
+^\[main.assertion\.3\] line 31 assertion one_tenth_ish < 0.2f: UNKNOWN
+^\[main.assertion\.4\] line 36 assertion 10.0f / five == 2.0f: SUCCESS
diff --git a/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c b/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c
index 3477023e956..7f29ebf1b01 100644
--- a/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c
+++ b/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c
@@ -1,8 +1,8 @@
 void test(int *x, int *y)
 {
-  assert(x);
-  assert(y);
-  assert(x == y);
-  assert(x != y);
-  assert(*x == *y);
+  __CPROVER_assert(x, "assertion x");
+  __CPROVER_assert(y, "assertion y");
+  __CPROVER_assert(x == y, "assertion x == y");
+  __CPROVER_assert(x != y, "assertion x != y");
+  __CPROVER_assert(*x == *y, "assertion *x == *y");
 }
diff --git a/regression/goto-harness/function_pointer_nullable/test.c b/regression/goto-harness/function_pointer_nullable/test.c
index 13a0c3eec61..fd05ac89bb3 100644
--- a/regression/goto-harness/function_pointer_nullable/test.c
+++ b/regression/goto-harness/function_pointer_nullable/test.c
@@ -1,15 +1,22 @@
-#include <assert.h>
 #include <stdlib.h>
 
 typedef int (*fptr_t)(void);
 
 void entry_point(fptr_t f, fptr_t f_but_may_be_null)
 {
-  assert(f != (void *)0);                 // expected to succeed
-  assert(f == (void *)0);                 // expected to fail
-  assert(f_but_may_be_null != (void *)0); // expected to fail
-  assert(f_but_may_be_null == (void *)0); // expected to fail
-  assert(f_but_may_be_null == (void *)0 || f() == f_but_may_be_null());
+  __CPROVER_assert(
+    f != (void *)0, "assertion f != (void *)0 - expected to succeed");
+  __CPROVER_assert(
+    f == (void *)0, "assertion f == (void *)0 - expected to fail");
+  __CPROVER_assert(
+    f_but_may_be_null != (void *)0,
+    "assertion f_but_may_be_null != (void *)0 - expected to fail");
+  __CPROVER_assert(
+    f_but_may_be_null == (void *)0,
+    "assertion f_but_may_be_null == (void *)0 - expected to fail");
+  __CPROVER_assert(
+    f_but_may_be_null == (void *)0 || f() == f_but_may_be_null(),
+    "assertion f_but_may_be_null == (void *)0 || f() == f_but_may_be_null()");
 }
 
 int f(void)
diff --git a/regression/goto-harness/function_pointer_nullable/test.desc b/regression/goto-harness/function_pointer_nullable/test.desc
index 659a84a28c5..28f85561d1b 100644
--- a/regression/goto-harness/function_pointer_nullable/test.desc
+++ b/regression/goto-harness/function_pointer_nullable/test.desc
@@ -3,10 +3,10 @@ test.c
 --harness-type call-function --function entry_point --function-pointer-can-be-null entry_point::f_but_may_be_null
 ^EXIT=10$
 ^SIGNAL=0$
-\[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS
-\[entry_point.assertion.2\] line \d+ assertion f == \(void \*\)0: FAILURE
-\[entry_point.assertion.3\] line \d+ assertion f_but_may_be_null != \(void \*\)0: FAILURE
-\[entry_point.assertion.4\] line \d+ assertion f_but_may_be_null == \(void \*\)0: FAILURE
+\[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0 - expected to succeed: SUCCESS
+\[entry_point.assertion.2\] line \d+ assertion f == \(void \*\)0 - expected to fail: FAILURE
+\[entry_point.assertion.3\] line \d+ assertion f_but_may_be_null != \(void \*\)0 - expected to fail: FAILURE
+\[entry_point.assertion.4\] line \d+ assertion f_but_may_be_null == \(void \*\)0 - expected to fail: FAILURE
 \[entry_point.assertion.5\] line \d+ assertion f_but_may_be_null == \(void \*\)0 || f\(\) == f_but_may_be_null\(\): SUCCESS
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/assert1/test.desc b/regression/goto-instrument/assert1/test.desc
index c2d2fa95ee8..9e2da3090fe 100644
--- a/regression/goto-instrument/assert1/test.desc
+++ b/regression/goto-instrument/assert1/test.desc
@@ -5,4 +5,4 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^[[:space:]]*IF
+^[[:space:]]*if
diff --git a/regression/goto-instrument/generate-function-body-havoc-params-call-sites/main.c b/regression/goto-instrument/generate-function-body-havoc-params-call-sites/main.c
index 465d78714a1..9552eb6a97e 100644
--- a/regression/goto-instrument/generate-function-body-havoc-params-call-sites/main.c
+++ b/regression/goto-instrument/generate-function-body-havoc-params-call-sites/main.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <string.h>
 
 struct S
 {
@@ -18,18 +18,22 @@ int main(void)
   int unchanged_parameter = 10;
   struct S my_struct = {.i = 10, .j = "10"};
   touches_parameter(&parameter, &unchanged_parameter, &my_struct, 4);
-  assert(parameter == 10);
-  assert(unchanged_parameter == 10);
-  assert(my_struct.i == 10);
-  assert(my_struct.j == "10");
+  __CPROVER_assert(parameter == 10, "assertion parameter == 10");
+  __CPROVER_assert(
+    unchanged_parameter == 10, "assertion unchanged_parameter == 10");
+  __CPROVER_assert(my_struct.i == 10, "assertion my_struct.i == 10");
+  __CPROVER_assert(
+    strncmp(my_struct.j, "10", 3) == 0, "assertion my_struct.j == \"10\"");
 
   parameter = 10;
   unchanged_parameter = 10;
   my_struct.i = 10;
   my_struct.j = "10";
   touches_parameter(&parameter, &unchanged_parameter, &my_struct, 4);
-  assert(parameter == 10);
-  assert(unchanged_parameter == 10);
-  assert(my_struct.i == 10);
-  assert(my_struct.j == "10");
+  __CPROVER_assert(parameter == 10, "assertion parameter == 10");
+  __CPROVER_assert(
+    unchanged_parameter == 10, "assertion unchanged_parameter == 10");
+  __CPROVER_assert(my_struct.i == 10, "assertion my_struct.i == 10");
+  __CPROVER_assert(
+    strncmp(my_struct.j, "10", 3) == 0, "assertion my_struct.j == \"10\"");
 }
diff --git a/regression/goto-instrument/generate-function-body-union-with-const-member/main.c b/regression/goto-instrument/generate-function-body-union-with-const-member/main.c
index 56913e9baa1..66bb122ef39 100644
--- a/regression/goto-instrument/generate-function-body-union-with-const-member/main.c
+++ b/regression/goto-instrument/generate-function-body-union-with-const-member/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 union WithConstMember {
   int non_const;
   const int is_const;
@@ -13,13 +11,21 @@ int main(void)
   union WithConstMember paramUnion;
   globalUnion.non_const = 10;
   paramUnion.non_const = 20;
-  assert(globalUnion.non_const == 10);
-  assert(globalUnion.is_const == 10);
-  assert(paramUnion.non_const == 20);
-  assert(paramUnion.is_const == 20);
+  __CPROVER_assert(
+    globalUnion.non_const == 10, "assertion globalUnion.non_const == 10");
+  __CPROVER_assert(
+    globalUnion.is_const == 10, "assertion globalUnion.is_const == 10");
+  __CPROVER_assert(
+    paramUnion.non_const == 20, "assertion paramUnion.non_const == 20");
+  __CPROVER_assert(
+    paramUnion.is_const == 20, "assertion paramUnion.is_const == 20");
   havoc_union(&paramUnion);
-  assert(globalUnion.non_const == 10);
-  assert(globalUnion.is_const == 10);
-  assert(paramUnion.non_const == 20);
-  assert(paramUnion.is_const == 20);
+  __CPROVER_assert(
+    globalUnion.non_const == 10, "assertion globalUnion.non_const == 10");
+  __CPROVER_assert(
+    globalUnion.is_const == 10, "assertion globalUnion.is_const == 10");
+  __CPROVER_assert(
+    paramUnion.non_const == 20, "assertion paramUnion.non_const == 20");
+  __CPROVER_assert(
+    paramUnion.is_const == 20, "assertion paramUnion.is_const == 20");
 }
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 36b0d3e34cf..20a9fdd226d 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -192,11 +192,23 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
       return convert_decl(target, upper_bound, dest);
 
     case ASSERT:
+    {
       system_headers.insert("assert.h");
       dest.add(code_assertt(target->get_condition()));
       dest.statements().back().add_source_location().set_comment(
         target->source_location().get_comment());
+
+      goto_programt::const_targett next = target;
+      ++next;
+      CHECK_RETURN(next != goto_program.instructions.end());
+      if(
+        next != upper_bound && next->is_assume() &&
+        target->get_condition() == next->get_condition())
+      {
+        ++target;
+      }
       return target;
+    }
 
     case ASSUME:
       dest.add(code_assumet(target->guard));
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index a154338c099..df753283404 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -849,6 +849,12 @@ void goto_convertt::do_function_call_symbol(
       error() << identifier << " expected not to have LHS" << eom;
       throw 0;
     }
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
+      function.source_location()));
   }
   else if(identifier == CPROVER_PREFIX "enum_is_in_range")
   {
@@ -1092,6 +1098,11 @@ void goto_convertt::do_function_call_symbol(
     t->source_location_nonconst().set_property_class(ID_assertion);
     t->source_location_nonconst().set_comment(description);
     // we ignore any LHS
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      false_exprt(), function.source_location()));
   }
   else if(identifier=="__assert_rtn" ||
           identifier=="__assert")
@@ -1130,6 +1141,11 @@ void goto_convertt::do_function_call_symbol(
     t->source_location_nonconst().set_property_class(ID_assertion);
     t->source_location_nonconst().set_comment(description);
     // we ignore any LHS
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      false_exprt(), function.source_location()));
   }
   else if(identifier=="__assert_func")
   {
@@ -1164,6 +1180,11 @@ void goto_convertt::do_function_call_symbol(
     t->source_location_nonconst().set_property_class(ID_assertion);
     t->source_location_nonconst().set_comment(description);
     // we ignore any LHS
+
+    // The C standard mandates that a failing assertion causes execution to
+    // abort:
+    dest.add(goto_programt::make_assumption(
+      false_exprt(), function.source_location()));
   }
   else if(identifier==CPROVER_PREFIX "fence")
   {