Andrea Mattavelli

@pietrobraione I actually don't understand your comment. Environment variables are IDE- and OS-independent, so why shouldn't they be IDE-friendly? Moreover, hard-coded paths are everything-unfriendly. A typical user wants to download...

> I can safely say that both MiniSat and CMS are fully deterministic. @ccadar and I observed yesterday that it seems that MiniSat uses some sort of seed: ``` $...

@delcypher I wonder if the misalignment between Alloc/Type/Expr size is peculiar to types with alignment only.

@kren1 We changed many things but not directly addressing this issue. It would be indeed interesting to understand which change introduced benefits. Can you please try to figure it out...

Shouldn't we just raise an error in the combination Z3+cvc?

@delcypher Ok, now that I read the code I understand your point. I agree with you and @ccadar, a solver-independent option is probably what it is better to use. At...

@delcypher It is a very good point. I believe KLEE was designed like that because the PC already describes the same behavior, with less constraints, with the intuition that "less...

Our regression test suite does not run the case studies.

@davidtr1037 your patches in the `handle-alloc` branch fix some of the issues for libtasn1, still CVE-2014-3467 fails a lot for non-concrete addresses. For example, ```bash amattave@phobos:/data/klee-slicing/klee-slicing-experiments/libtasn1/CVE-2014-3467$ /data/klee-slicing/klee-build/bin/klee --exit-on-error-type=Ptr --error-location=decoding.c:709 --libc=uclibc...

@davidtr1037 Suppose that I want to skip function `f(a,b)`. If both `a` and `b` are concrete, we don't need to skip the function, slice, etc. We can simply execute it....