We rebuilt KLEE again and now it works with the latest version of STP.
KLEE with STP-r940 is still not working but this should be fine now as
we have a working version. Thank you all for the suggestions.
If you are interested in our configuration and how we build and run
KLEE, it is detailed
Dan, the message starts with We tried two versions of STP (r940 and the
latest) :)
Yes but
- I was asking if you had STP built with assertions when trying to
reproduce the issue. It is obvious
the the OP had assertions enabled when they ran their build of KLEE.
- The stacktrace shown by the
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?
Best,
Cristian
On 26/02/15 09:52, Yu-Fang Chen wrote:
We tried two versions of STP (r940 and the latest) and KLEE gives us
the
On 27 February 2015 at 10:52, Cristian Cadar c.ca...@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
On 27/02/15 11:11, Dan Liew wrote:
On 27 February 2015 at 10:52, Cristian Cadar c.ca...@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
You may want to check if you have stack limit set to unlimited (you can do this
using ulimit -s).
Best regards,
Tomek
On 27 Feb 2015, at 10:52, Cristian Cadar c.ca...@imperial.ac.uk wrote:
I cannot reproduce this on my machine. Can you open an issue at
We tried two versions of STP (r940 and the latest) and KLEE gives us
the message BVTypeCheck: terms in atomic formulas must be of equal
length with both versions.
Below is the program we run using klee and the output.
PROGRAM:
#include assert.h
#include klee/klee.h
#define N 5
int avg (int
