Corrected divbin verdict (from #808) and its correct version

[divyeshunadkat]

The assertion in the divbin program is violable. Counter example was obtained using a bounded model checker and manually verified. Hence this pull request changes the verdict of this program. Also, corrected program version divbin2 with verifiable assertion is added.

Benchmarks from PR #808
Similar issues discussed in PR #813
Partial corrections issued in PR #837

• programs added to new and appropriately named directory

• license present and acceptable (either in separate file or as comment at beginning of program)

• contributed-by present (either in README file or as comment at beginning of program)

• programs added to a .set file of an existing category, or new sub-category established (if justified)

• intended property matches the corresponding .prp file

• programs and expected answer added to a .yml file according to task definitions

• architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
• original sources present
• preprocessed files present
• preprocessed files generated with correct architecture
• Makefile added with correct content and without overly broad suppression of warnings

[divyeshunadkat]

Assertion within the loop in the program divbin to is violable as depicted by the following counter-example:

INITIALIZATION
A = 2470896015 B = 1074551579

Before 0th iteration of the second loop
b = 3316756480 r = 2470896015 q = 0
q * b + r = 2470896015

Before 1th iteration of the second loop
b = 1658378240 r = 812517775 q = 1
q * b + r = 2470896015

Before 2th iteration of the second loop
b = 829189120 r = 812517775 q = 2
q * b + r = 2470896015

Before 3th iteration of the second loop
b = 414594560 r = 397923215 q = 5
q * b + r = 2470896015

Before 4th iteration of the second loop
b = 207297280 r = 190625935 q = 11
q * b + r = 2470896015

Before 5th iteration of the second loop
b = 103648640 r = 86977295 q = 23
q * b + r = 2470896015

Before 6th iteration of the second loop
b = 51824320 r = 35152975 q = 47
q * b + r = 2470896015

Before 7th iteration of the second loop
b = 25912160 r = 9240815 q = 95
q * b + r = 2470896015

Before 8th iteration of the second loop
b = 12956080 r = 9240815 q = 190
q * b + r = 2470896015

Before 9th iteration of the second loop
b = 6478040 r = 2762775 q = 381
q * b + r = 2470896015

Before 10th iteration of the second loop
b = 3239020 r = 2762775 q = 762
q * b + r = 2470896015

Before 11th iteration of the second loop
b = 1619510 r = 1143265 q = 1525
q * b + r = 2470896015

Before 12th iteration of the second loop
b = 809755 r = 333510 q = 3051
q * b + r = 2470896015

Before 13th iteration of the second loop
b = 404877 r = 333510 q = 6102
q * b + r = 2470892964

ASSERTION FAILED as the value of q*b+r != A at the beginning of 13th iteration of the second loop.

This issue occurs because of the rounding error when the variable 'b' is an odd number and is divided by 2.

Before 12th iteration b = 809755, q = 3051, resulting in q*b = 2470562505

In the 12th iteration b is divided by 2 and q is multiplied by 2. Nothing else changes.

However, before 13th iteration b = 404877, q = 6102 results in qb = 2470559454 creating a difference of 3051 in the values of qb due to rounding of b by 0.5

Corrected program ensures that the value of 'b' starts with value 1 and is always an even number that is a multiple of 2, hence avoiding the round off error.

[mikhailramalho]

Both ESBMC and CBMC find property violations in the divbin.c benchmark.

However, I think you can drop the pre-processed file and use only the .c file.

[dbeyer]

Thanks @divyeshunadkat for the correction, and thanks @mikhailramalho for the suggestion.
I propose to create a new pull request for dropping the .i file, such that I can merge and make it available to others.