Unexpected verification result related to unsigned char calculation

[muchang]

#include <assert.h>
unsigned char x = 50;
short y = -5;

int main ()
{
  x /= y;
  if (x != (unsigned char) -10)
    {assert(0); } 
return 0; }

CBMC version: 5.10
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc <file.c>
What behaviour did you expect: Result in SUCCESS (proofed by compiling with gcc and Compcert)
What happened instead: [main.assertion.1] assertion 0: FAILURE

[kroening]

Many thanks, test added.