You can do a lot with Symbolic Execution. Bug-reproduction for example. Say your customer remarks on a weird state if the system. You put a 'stop condition' as

You can do a lot with Symbolic Execution. Bug-reproduction for example. Say your customer remarks on a weird state if the system. You put a 'stop condition' as 'the system is in the state the customer described' and ask 'how'? You get a list of input & their values. Aaaaah that's how :-). Also if you record/print intermediate values you can use them as complexity reduction for your search. Also, for minimal log/trace placement it's actually fun to use.