Zvonimir Rakamaric

We should really do this properly since it often causes confusion for our users.

Once a new release of Boogie gets pushed out, we should be able to remove this line: https://github.com/smackers/smack/blob/develop/bin/build.sh#L386

I am not sure why it is a module pass right now.

SMACK does not catch freeing of stack locations as an invalid-free error

3

Here is a simple regression for this: ``` #include "smack.h" int main(void) { int x = __VERIFIER_nondet_int(); int *y = &x; free(y); return 0; } ``` This regression should fail,...

Corral throws a weird exception on those benchmarks.

It seems that Boolector currently supports QF_AUFBV, which should be good enough for many SMACK benchmarks. And it regularly beats Z3 in this category. So it would be good to...

Currently `malloc` cannot fail, while `calloc` can nondeterministally fail and return `0`. We should make that uniform, and maybe have a command like option that turns on nondeterministic failures.

It is I guess well-known that Z3 does not do super well when bitvectors are mixed with arrays/functions/quantifiers. Hence, different tactics can be used to first compile away everything into...

Our model of pthreads mostly leverages C `int` type for various pthreads types and structure fields. That is fine when mathematical integers are used to model C integers. However, when...

While working on pull request #508, I realized that the following if condition that leads to regions being generated is maybe not needed https://github.com/smackers/smack/blob/691b231dfd6ffc00924c533164c31a6596d3b84c/lib/smack/Regions.cpp#L350-L351 The only theory I have for...