On Tue Feb 9 11:33:00 GMT 2021, Cristian Cadar wrote: > printf is run concretely by default (you can add -DKLEE_SYM_PRINTF > when compiling KLEE's uclibc to change this) Do you recall the reason for that default, i.e. what are the potential drawbacks of enabling symbolic printf in KLEE's µClibc?