add an option --fail-on-solver-unknown

[zapashcanon]

instead of simply not exploring the path (in symbolic choice)

it never happened AFAIK but as a future-proof check

[krtab]

I think in general the cli option should be more abstract and indicate whether the user want to guarantee the absence of bugs or quickly find one (verifier vs bug-finder )

[zapashcanon]

Indeed, this is related to #450

[filipeom]

I'll just throw in my two cents. I generally prefer over-approximating analyses, meaning they might report bugs even when none exist. So here, perhaps the default behaviour should be to always report Unknown solver queries as potential failures. This way, we don't compromise on soundness.

Thus, the option would be the other way around: --no-fail-on-unknown, making Owi more complete but less sound.