Include tests from reported issue cbmc#5952.

This is including two tests from #5952,
one of which succeeds demonstrating that the issue is now fixed,
and the other one is failing, marked so as `broken-smt-backend`, presumably
because of the `__CPROVER_r_ok` within an `assume` context.

Author: NlightNFotis

regression/cbmc/issue_5952_soundness_bug_smt_encoding/original_repro.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool validate(const char *data, unsigned allocated)
+{
+  bool check_1 = (data == NULL == > allocated == 0);
+  bool check_2 = (allocated != 0 == > __CPROVER_r_ok(data, allocated));
+  return check_1 && check_2;
+}
+
+void main()
+{
+  char *data;
+  unsigned allocated;
+
+  data = (allocated == 0) ? NULL : malloc(allocated);
+
+  __CPROVER_assume(validate(data, allocated));
+
+  assert(validate(data, allocated));
+}

regression/cbmc/issue_5952_soundness_bug_smt_encoding/short.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *data;
+  data = nondet() ? malloc(1) : malloc(2);
+  assert(__CPROVER_OBJECT_SIZE(data) <= 2);
+}

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+original_repro.c
+--smt2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+[main.assertion.\d] line \d+ assertion validate(data, allocated): SUCCESS
+--
+[main.assertion.\d] line \d+ assertion validate(data, allocated): FAILURE
+--
+This is the original code that demonstrates the issue described in
+https://github.com/diffblue/cbmc/issues/5952

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc

@@ -0,0 +1,12 @@
+CORE
+short.c
+--smt2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+[main.assertion.\d] line \d assertion __CPROVER_OBJECT_SIZE(data) <= 2: SUCCESS
+--
+[main.assertion.\d] line \d assertion __CPROVER_OBJECT_SIZE(data) <= 2: FAILURE
+--
+This is the reduced version of the issue described in
+https://github.com/diffblue/cbmc/issues/5952