Zvonimir Rakamaric

While we are at it, it would be good to also add a regression with `__SMACK_value`.

I think in the long run we should split SMACK headers into C and C++ specific ones, with maybe a top-level shared header.

There are two related things happening here. 1. We have this hacky heuristic in SMACK that searches for large constants in SVCOMP benchmarks and replaces them with small numbers to...

When I run SMACK with `--unroll=3` it finds this bug. How did you run it?

Let me implement a switch that turns it off. I'll let you know once that is done. This is also related to issue #159.

Given that the deadline has passed, I am of the opinion that all benchmarks with open issues should be moved into the todo folder and discussed in detail after the...

@mutilin It could as well be that other benchmarks contain similar problems. It is hard to say why SMACK is not discovering these problems in other benchmarks. Maybe they are...

Why don't you run it without this 90 seconds time out? This is not the competition, but rather an attempt to fix bugs in SV-COMP benchmarks, and so enforcing this...

For SVCOMP, the rules say that verifiers have to take care of modeling standard library functions. So no definitions will be provided for standard library functions. I suspect that testing...

I guess that would be institutional knowledge that is probably not really specified anywhere in the rules. In my experience, there are quite a few things like that that you...