Zero-termination assertion fails on zero-terminated strings

[alexoltean61]

Possibly related to #8310.

CBMC version: 5.95.1
Operating system: Both Ubuntu 22.04.4 and Windows 11 22H2
Exact command line resulting in the issue:
I have the following C program in a file named bug1.c:

int strcmp(const char *s1, const char *s2);

void f1(char *str1, char *str2)
{
  strcmp(str1, str2);
}

void f2(int trouble, char *str1, char *str2)
{
  strcmp(str1, str2);
}

void test1()
{
  f1("abc", "def");
}

void test2()
{
  f2(0, "abc", "def");
}

void test3()
{
  int len1, len2;
  __CPROVER_assume(len1 > 0 && len2 > 0);
  char str1[len1];
  char str2[len2];
  str1[len1-1] = 0;
  str2[len2-1] = 0;

  f1(str1, str2);
}

void test4()
{
  int len1, len2;
  __CPROVER_assume(len1 > 0 && len2 > 0);
  char str1[len1];
  char str2[len2];
  str1[len1-1] = 0;
  str2[len2-1] = 0;

  int trouble;
  f2(trouble, str1, str2);
}

I run the following commands:

cbmc bug1.c --function test1 --string-abstraction
cbmc bug1.c --function test2 --string-abstraction
cbmc bug1.c --function test3 --string-abstraction
cbmc bug1.c --function test4 --string-abstraction

What behaviour did you expect:
All four verification cases pass.

What happened instead:
Verification of test2 and test4 fails, with the following unmet assertion:

** Results:
<builtin-library-strcmp> function strcmp
[strcmp.precondition.1] line 14 strcmp zero-termination of 1st argument: SUCCESS
[strcmp.precondition.2] line 16 strcmp zero-termination of 2nd argument: FAILURE

Indeed, memory-safe strcmp requires both its arguments to be null-terminated. However, all my test harnesses meet this assumption already.