[klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)

Dan Liew dan at su-root.co.uk
Fri Feb 27 11:11:47 GMT 2015


On 27 February 2015 at 10:52, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> I cannot reproduce this on my machine.  Can you open an issue at
> https://github.com/klee/klee/issues, giving more details on your
> configuration and how you ran KLEE?

Do you have STP built with assertions? They've been enabled by default
in the latest upstream STP but I'm not sure if this the case for r940.

I think we should stop recommending people using r940, it's really
old, doesn't even build on new linux distros and has bugs that have
been fixed in the upstream version.



More information about the klee-dev mailing list