--warningAsError[UnsafeDefault]:"on"
--warningAsError[ProveInit]:"on"