Hi Michael, Thanks very much for reporting this! I can reproduce this bug.
This is a recent regression that crept in when we switched to using llvm raw_ostreams rather than the std:: streams. I've fixed this in my own branch (and added a test case) and have issued a pull request (https://github.com/klee/klee/pull/133) to the main KLEE repository. Until this is merged (I can't do this) you can grab my changes by doing $ git checkout -b temporary_branch_name $ git pull [email protected]:delcypher/klee.git fix_empty_error_report which should hopefully fix your issue. Thanks, Dan _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
