Incorrect output when --max-violations is greater than 1

[shaobo-he]

For example,

#include "smack.h"

int main() {
  assert(2 == 3);

  assert(4 == 5);
  return 0;
}

If SMACK is invoked as smack test.c --max-violations 10, then the output is SMACK found no errors with unroll bound 1.

[zvonimir]

Is this because LLVM maybe compiles away these assertions or something like that? What is the root cause of this? Is the generated Boogie file ok?

[shaobo-he]

Is this because LLVM maybe compiles away these assertions or something like that? What is the root cause of this? Is the generated Boogie file ok?

No, this is because Corral's output shows one error and one successful verification (this can be seen when -v is enabled). Corral turns assert 2 == 3 into assume 2 == 3 and continues the verification. Our verification_result function first captures the successful verification message and returns verified.

Btw, SMACK's output only shows SMACK found an error, which seems inconsistent with --max-violations being greater than one.