Bug: Reachable error call not found

[Novak756]

Basic Info

• Version: 0.2.3-dev-921ad1f
• Java Version: 17.0.7
• Operating System: Ubuntu 20.04.6 LTS (Focal Fossa)
• Kernel: 5.15.90.1-microsoft-standard-WSL2
• Input file: bug,c, containing the following:

  
  extern void __VERIFIER_error(void);
  extern unsigned char __VERIFIER_nondet_uchar(void);

int main(){ unsigned char uc = VERIFIER_nondet_uchar(); if((unsigned int) ((unsigned int)(((unsigned int)(((unsigned int) uc) + ((unsigned int)(((unsigned int) 4294967295) * 1)))) >> ((unsigned int) 2))) < (unsigned int) 8){ VERIFIER_error(); } return 0; }

* Settings: Ultimate.py --architecture 64bit --file bug.c --spec unreach.prp (Containing `CHECK( init(main()), LTL(G ! call(reach_error())) )
`)
* Toolchain: Fails on Taipan, Automizer, GemCutter and Kojak
* Logs for each tool: [logs.zip](https://github.com/ultimate-pa/ultimate/files/12233833/logs.zip)

### Description 
The __VERIFIER_error(); is reachable, for example with uc := 32. However Ultimate returns TRUE, indicating that the error cannot be reached.

[Heizmann]

Thanks for the bug report. If you run ./Ultimate -tc config/AutomizerReach.xml -s config/svcomp-Reach-64bit-Automizer_Bitvector.epf -i bug.c you will get the correct result. It seems that our integer-based analysis fails to compute modulo 2^{32} in rare cases related to a shift operation. I will have a closer look at the problem in the next days.

[schuessf]

I fixed it, there was indeed a missing modulo in the case, where the second operand of the right-shift is a constant.