================
@@ -213,6 +215,15 @@ ANALYZER_OPTION(
"400'000 should on average make Z3 queries run for up to 100ms on modern "
"hardware. Set 0 for unlimited.", 0)
+ANALYZER_OPTION(
+ unsigned, Z3CrosscheckRetriesOnTimeout,
+ "crosscheck-with-z3-retries-on-timeout",
+ "Set how many times the oracle is allowed to retry a Z3 query. "
+ "Set 0 for not allowing retries, in which case each Z3 query would be "
+ "attempted only once. Increasing the number of retries is often more "
----------------
steakhal wrote:
I considered this. But then the semantic would be unclear if they set the value
0 for it yet they "enable" Z3 refutation. It would be confusing to see that all
reports are discarded (because none of them are "SAT" or "accepted") yet they
enabled Z3 refutation.
I find that configuration combination, or even the value zero for this option a
trap.
To resolve this, I could see 2 options:
1) Drop the `crosscheck-with-z3` and just use this
`crosscheck-with-z3-attempts-on-timeout` to imply if Z3 crosscheck should be
enabled or not.
2) Keep the current what I propose in this patch. (My preference)
https://github.com/llvm/llvm-project/pull/120239
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
