--refine imprecision

[Novak756]

Hi, I know this feature is experimental so feel free to close this if it is not helpful.
In the following program cbmc --refine incorrectly claims that the error is reachable:

extern void __VERIFIER_error();
extern unsigned long __VERIFIER_nondet_ulong();
int main() {
    unsigned long n = __VERIFIER_nondet_ulong();
    if (1 % (n | 18446744073709551615ULL) == 0){
        __VERIFIER_error();
    }
} 

running without the --refine flag gives the correct result.

CBMC version: Built from commit 13a452d
Operating system: Linux (Ubuntu 20.04)
Exact command line resulting in the issue: cbmc --refine test.c
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: [main.assertion.1] line 6 assertion: FAILURE