[klee-dev] Fatal Error in BVTypeCheck

[Martin Nowack]

Hi,

Can you write your setup of KLEE and which LLVM version you use?

What are the arguments to start KLEE?

Cheers,
Martin


On 20 May 2014, at 04:43, Jingde Liu <liujingde2008 at gmail.com> wrote:

> Hi everyone,
> 
> I encounter the following problem when using KLEE to execute a simple program.
> 
> The code of the program is as bellow:
> ________________________________________
> int test(int x) { 
>     int a; 
>     if(x>100)
>     {
>         a = x / 100; 
>         if(a > 10) 
>             return x; 
>     }
>     return 0; 
> } 
> _________________________________________
> After ran it using KLEE, it showed this error:
> Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length
> But when I ran it using Cloud9, it was OK.
> I don't know how to handle this problem.
> Any help is truly appreciated.
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140521/75bcec2c/attachment.sig>