[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

Gábor Horváth via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Tue Mar 21 05:59:21 PDT 2017


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





More information about the cfe-commits mailing list