[klee-dev] Possibly incorrect models generated

[Frank Busse]

Hi,


On Sat, 10 Nov 2018 07:07:13 +0000
Alberto Barbaro <barbaro.alberto at gmail.com> wrote:

> I feel I'm missing something because, for instance, I cannot see the
> case where a = 0 and another = 12.

That's the 2nd if statement:

| if ( a == 77 ) {           // a=77, another=?[0]       = ktest 1
| } else {                   // (a!=77)
|   if ( another == 12 ) {   // a!=77[0], another=12     = ktest 3
|   } else {                 // a!=77[0], another!=12[0] = ktest 2

Seems fine to me (values generated by solver in brackets).


Kind regards,

Frank