I sometimes see states terminated with the error message "concretized symbolic size". Since this produces a test*.err file in Klee's output, I assumed it could be related to a possible bug found by Klee. However, when reading the source code in Executor::executeAlloc() I see that in case a large symbolic value is possible, the execution will fork and will create one state in which malloc() returns 0 and another state which is terminated with this error.
My question is what is the purpose of the second state? Does it mean there could be a possible bug or just to highlight that there was a case in which a symbolic size was concretized? Thanks, Cristi
