From 08c5cde0d70837f4c7f275bd8c34608212599f63 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 3 Apr 2021 16:15:40 +0000
Subject: [PATCH 1/2] Regression tests: use __CPROVER_assert when multiple
 properties may fail

C's assert() should result in an abort() when the asserted condition
evaluates to false. If we want to test multiple properties, including
some failing ones, use __CPROVER_assert to not rely on any modelling of
assert() that does not result in an abort().
---
 regression/cbmc-cover/simple_assert/main.c    |  4 +-
 regression/cbmc-cover/simple_assert/test.desc |  2 -
 .../cbmc-incr-oneloop/multiple-asserts/test.c |  4 +-
 .../cbmc/Quantifiers-not-exists/fixed.c       | 30 +++++++----
 .../cbmc/Quantifiers-not-exists/fixed.desc    | 12 ++---
 regression/cbmc/double_deref/double_deref.c   |  4 +-
 .../double_deref/double_deref_single_alias.c  |  4 +-
 .../double_deref/double_deref_with_cast.c     |  4 +-
 .../double_deref_with_cast_single_alias.c     |  4 +-
 .../double_deref/double_deref_with_member.c   |  4 +-
 .../double_deref_with_member_single_alias.c   |  4 +-
 .../double_deref_with_pointer_arithmetic.c    |  5 +-
 ...ref_with_pointer_arithmetic_single_alias.c |  5 +-
 regression/cbmc/json-interface1/main.c        |  8 ++-
 regression/cbmc/json-interface1/test.desc     |  2 +-
 regression/cbmc/multiple-goto-traces/main.c   | 10 ++--
 regression/cbmc/r_w_ok5/main.c                | 17 +++----
 regression/cbmc/r_w_ok6/main.c                | 13 +++--
 .../cbmc/reachability-slice-interproc/test.c  |  4 +-
 regression/cbmc/xml-interface1/main.c         |  8 ++-
 regression/cbmc/xml-interface1/test.desc      |  2 +-
 .../goto-analyzer/command_line_01/main.c      |  6 +--
 .../goto-analyzer/command_line_01/test.desc   |  4 +-
 .../goto-analyzer/command_line_02/main.c      |  6 +--
 .../goto-analyzer/command_line_02/test.desc   |  4 +-
 .../constant_propagation_18/main.c            |  4 +-
 .../constant_propagation_18/test-vsd.desc     |  2 +-
 .../constant_propagation_18/test.desc         |  2 +-
 .../constant_propagation_19/main.c            |  4 +-
 .../constant_propagation_19/test-vsd.desc     |  2 +-
 .../constant_propagation_19/test.desc         |  2 +-
 .../main.c                                    |  4 +-
 .../test.desc                                 |  2 +-
 .../main.c                                    | 16 +++---
 .../test.desc                                 |  8 +--
 .../constant_propagation_two_way_1/main.c     |  4 +-
 .../constant_propagation_two_way_1/test.desc  |  2 +-
 .../context_sensitivity_02/main.c             |  4 +-
 .../context_sensitivity_04/main.c             |  6 +--
 .../context_sensitivity_05/main.c             | 51 ++++++++++++-------
 .../main.c                                    |  8 ++-
 .../goto-analyzer/flow-insensitive-if/main.c  |  8 ++-
 .../main.c                                    |  6 +--
 .../goto-analyzer/flow-sensitive-if/main.c    |  8 ++-
 .../goto-analyzer/history-output/main.c       |  4 +-
 .../intervals_simple-loops/main.c             |  5 +-
 .../intervals_simple-loops/test.desc          |  4 +-
 .../local_control_flow_history_01/main.c      | 10 ++--
 .../local_control_flow_history_02/main.c      | 10 ++--
 .../local_control_flow_history_03/main.c      |  5 +-
 .../local_control_flow_history_04/main.c      | 11 ++--
 .../local_control_flow_history_05/main.c      |  5 +-
 .../local_control_flow_history_06/main.c      |  5 +-
 .../main.c                                    |  4 +-
 .../test-intervals-constants.desc             |  2 +-
 .../test-intervals-top-bottom.desc            |  2 +-
 .../test-intervals-value-sets.desc            |  2 +-
 .../goto-analyzer/pointer-dereference/main.c  |  4 +-
 .../pointer-dereference/test-constants.desc   |  2 +-
 .../pointer-dereference/test-top-bottom.desc  |  2 +-
 .../pointer-dereference/test-value-sets.desc  |  2 +-
 .../main.c                                    |  4 +-
 .../test-intervals-constants.desc             |  2 +-
 .../test-intervals-top-bottom.desc            |  2 +-
 .../test-intervals-value-sets.desc            |  2 +-
 .../pointer-write-through/main.c              |  4 +-
 .../pointer-write-through/test-constants.desc |  2 +-
 .../test-top-bottom.desc                      |  2 +-
 .../test-value-sets.desc                      |  2 +-
 .../sensitivity-function-call-array/main.c    | 20 ++++----
 .../sensitivity-function-call-opaque/main.c   | 18 ++++---
 .../sensitivity-function-call-pointer/main.c  | 12 ++---
 .../main.c                                    |  6 +--
 .../main.c                                    | 13 ++---
 .../sensitivity-function-call-varargs/main.c  |  5 +-
 .../goto-analyzer/value-set-simple/main.c     | 35 ++++++++-----
 .../goto-analyzer/value-set-structs/main.c    | 41 ++++++++-------
 .../main.c                                    | 10 ++--
 .../test.desc                                 |  8 +--
 .../test.c                                    | 10 ++--
 .../function_pointer_nullable/test.c          | 19 ++++---
 .../function_pointer_nullable/test.desc       |  8 +--
 .../main.c                                    | 22 ++++----
 .../main.c                                    | 26 ++++++----
 84 files changed, 326 insertions(+), 339 deletions(-)

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/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_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/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");
 }

From 76491eb21d9480eccc12dd28d444c18102da29a2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 3 Apr 2021 16:15:52 +0000
Subject: [PATCH 2/2] Abort after failing C assert

The C standard specifies behaviour of the "assert" macro as resulting in
an abort when the condition does not evaluate to true. Implement this
behaviour by inserting assume(0) after assert(0).

Fixes: #5505
---
 regression/cbmc/Bool5/test.desc              |  2 +-
 regression/cbmc/r_w_ok1/test.desc            |  2 +-
 regression/goto-instrument/assert1/test.desc |  2 +-
 src/goto-instrument/goto_program2code.cpp    | 12 +++++++++++
 src/goto-programs/builtin_functions.cpp      | 21 ++++++++++++++++++++
 5 files changed, 36 insertions(+), 3 deletions(-)

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/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/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/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")
   {