xazax.hun added inline comments.
================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:60 + // Set timeout to 15000ms = 15s + Z3_set_param_value(Config, "timeout", "15000"); + } ---------------- Sorry for being a bit late in the party, I was wondering whether this timeout can be a source of non-determinism. The constraint solver might get lucky or unlucky based on the load or the underlying hardware to solve some of the constraints. We might end up with different results over different runs which can be confusing for the users. Is there any other way, to set something like a timeout, like limiting the number of steps inside the solver? https://reviews.llvm.org/D28952 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
