reduces the default timeout back to 16 ms (#1211)

It looks like that setting it to high makes the symbolic executor very
slow, as instead of discarding overly big formulas we spend more time
on solving it, rather than exploring other states. It is probably, why
our tests on symbolic executor are failing, though can't say for sure,
it is hard to bisect this issue, given that z3 timing is significantly
non-deterministic.

Author: ivg

plugins/primus_symbolic_executor/primus_symbolic_executor_main.ml

@@ -11,7 +11,7 @@ let cutoff = Extension.Configuration.parameter
     ~doc:"The number of times the same branch is retried."
 
 let timeout = Extension.Configuration.parameter
-    Extension.Type.(int =? 1000)
+    Extension.Type.(int =? 16)
     "timeout"
     ~doc:"The number of milliseconds alloted to the SMT solver to find
     a model"
@@ -166,9 +166,10 @@ end = struct
 
   let () = Z3.set_global_param "parallel.enable" "true"
 
+
   let ctxt = Z3.mk_context [
       "model", "true";
-      "timeout", "1000";
+      "timeout", "16";
     ]
 
   let set_timeout ms =