Paul Marinescu

Results 3 issues of Paul Marinescu

Right now the `--max-solver-time` option accepts a double argument. However, that argument is truncated to an integer before calling the solver because the timer is enforced by means of `alarm(unsigned...

Feature Request

The assertion in the program below should never fail, but klee does not properly update variable `zero` after the `read` call. The current implementation never picks up external changes to...

bug

Why does klee report an out of bound pointer on the call to `fail`? Seems to happen during the implicit cast to `basic_ios` ``` #include int main() { std::ifstream f("somefile");...

bug