Hi, In 2013, KLEE didn't support arrays with a symbolic size : http://mailman.ic.ac.uk/pipermail/klee-dev/2013-April/000116.html Is it still the case? If yes, how does the -max-sym-array-size option work? Does it simply replace a symbolic size by the upper bound specified? Thanks a lot, Aymeric Fromherz