I found a blog post with a succinct explanation.

> KLEE [runs] a program considering its input(or some other variables) to be symbols instead of concrete values like 100 or “cacho”. In very few words, a symbolic execution runs through the code propagating symbols and conditions; forking execution at symbol dependant branches and asking the companion SMT solver for path feasibility or counter-examples.

https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/

KLEE is a symbolic execution engine. You can use it to analyse your program. A symbolic execution considers all possible values for all variables. E.g.:

   int x = readIntFromIO(); // -2147483648 to 2147483647

On branches constraints are added.

    if(x < 3) {
        // -2147483648 to 2
    } else {
        // 3 to 2147483647
    }

In this way all possible paths of the program are considered. When the execution terminates, e.g. on reaching a abort() or fail() statemant, a constraint solver calculates the input values to reach this statement. This values could be considers as test cases.

You can add assert() statements to your code for expressions (e.g. assert(x != 3) ) that you assume to be an inconsistent states and solver will give you test cases for this.