CBMC stucks with --unsigned-overflow-check

[cradiator]

CBMC version: 5.94.0
Operating system: Linux
Exact command line resulting in the issue:
CBMC will stuck with following program and command

cbmc --function harness --unsigned-overflow-check main.c

typedef unsigned long long u64;

#define U64_MAX		((u64)~0ULL)

void harness() {
    unsigned long long nents;
    unsigned long long stride;
    unsigned long long max_stride;

    if (nents == 0 || nents > 100000)
		return;

    max_stride = U64_MAX / nents;
	if (stride > max_stride)
		return;

    unsigned long long result = nents * stride;
    
    return;
}

What behaviour did you expect: Show verification result
What happened instead: Stuck

[thomasspriggs]

The size of the search space for the value of nents in combination with the division and multiplication leads to a long processing time. If for instance I take your example and add in if (nents > 100 && nents < 999900) return;, then it will execute much faster.