stoke bounded validator sometimes performs 0 SMT queries without telling the user

[stefanheule]

Stoke should print a warning if no comparisons are performed in the bounded validator, or have it print statistics on the number of paths found in the target/rewrite.

[bchurchill]

Actually, I'm realizing I was wrong about this. Your benchmark does have a path even with bound 1 that goes all the way through, it's just that it's not a feasible path. The SMT solver is making queries, but they're returning UNSAT because it's not possible for the paths to actually be executed.

All this to say: I've implemented this check in a branch (issue-976) but it doesn't actually give the warning on your benchmark. It does, however, warn that --bound 0 does nothing, so that seems worthwhile. Should we merge this?

[bchurchill]

A more meaningful thing we could do is make extra queries to the SMT solver to check if the paths are feasible. We would then users if no feasible pairs of paths were tested. This would be easy to implement too. But, we would double the number of SMT queries in the worst case. Maybe this would be suitable for a debugging option.

[stefanheule]

Yeah, having it as an option seems useful, and I would even argue having it on by default might be useful, too. It would in general be great if we could output some statistics to let the user know what was going on.