Wrong result is given for the unreach-call property

[leventeBajczi]

Config 1: --strategy DIRECT --maxenum 1 --loglevel RESULT --refinement SEQ_ITP --lbe LBE_SEQ --search ERR --prunestrategy FULL --predsplit ATOMS --cex-monitor DISABLE --domain EXPL
Problem17_label11.yml

Config 2: --strategy DIRECT --maxenum 1 --loglevel RESULT --refinement SEQ_ITP --lbe LBE_SEQ --search ERR --prunestrategy FULL --predsplit ATOMS --cex-monitor DISABLE --domain PRED_CART
Problem10_label30.yml, Problem11_label40.yml, Problem15_label49.yml

[s0mark]

The reason behind the wrong answers appears to be that the semantics of integer division (/) and modulo (%) for negative numbers are different in C and in Z3, as well as in Theta which follows the Z3 semantics in its core (e.g. IntLitExpr):

expression	C /	Z3 div
5 / 3	1	1
5 / -3	-1	-1
-5 / 3	-1	-2
-5 / -3	1	2

expression	C %	Z3 mod	Z3 rem
5 % 3	2	2	2
5 % -3	2	2	-2
-5 % 3	-2	1	1
-5 % -3	-2	1	-1

[s0mark]

I fixed the integer division and modulo problems in #230. I ran Theta with the configurations and the tasks mentioned in the issue, it no longer gives wrong answers to them.

This issue brings up the possibility of further discrepancies between the semantics of C, Theta and the solvers: the sdiv/srem and udiv/urem operators for bitvectors might also be effected.

[leventeBajczi]

Thanks! Closing.