Hello, I'm attempting to modify the constraints KLEE adds to states in hopes of getting better path merging. I noticed when KLEE comes across an assignment, rather than adding a constraint about the variable being assigned to, KLEE updates the state's stack information to reflect this assignment. I'm trying to figure out how the solver uses this information when solving constraints, but I couldn't find the stack being passed to the solver at any point. It looks like the TimingSolver only passes the constraints and the expression to the Solver. Where does KLEE's Solver take variable information into account?
Thanks, Jonathan
