llreve

llreve copied to clipboard

Trace example fails on https://formal.kastel.kit.edu/projects/improve/reve/?ex=redis%2Ftrace with missing header: ``` /tmp/prog110123-1566.c:1:10: fatal error: 'lua.h' file not found #include ^~~~~~~ 1 error generated. ERROR: Couldn’t execute action ```

def-

If `-init-pred` is used as command-line parameter, the program produces illegal SMT2 code which has nested `assert` commands. ```` (assert (assert (forall ((n$1_0 Int) (n$2_0 Int)) (=> (IN_INV n$1_0 n$2_0)...

mattulbrich

wrong output for programs with printf function

2

Input C file contents- `#include int main(){ printf("hello"); return 0; }` and `#include int main(){ printf("bye"); return 0; }` `./llreve -I /usr/lib/gcc/x86_64-linux-gnu/7/include/ " + "./"+file+ " ./teacher_solution.c -o reve.smt2` Output-...

akhutail

Incorrect result for swab example using Z3

1

Z3 returns sat here while we would expect unsat. Not yet sure what’s going on here. The generated SMT looks correct.

cocreature

Assertion failure in llreve-dynamic

2

Hej, I tried to use the llreve-dyamic tool on the following example: ``` extern int __mark(int); void send(int *to, int *from, int count) { do { /* count > 0...

mattulbrich