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

Cristian Cadar c.cadar at imperial.ac.uk
Fri Feb 27 11:16:21 GMT 2015


On 27/02/15 11:11, Dan Liew wrote:
> 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.

Dan, the message starts with "We tried two versions of STP (r940 and the 
latest)" :)

Cristian




More information about the klee-dev mailing list