Klever

When Core generates complicated verification tasks that could not be solved quickly by task workers I observe the situation when Native Scheduler reserves most memory and thinks that it solves many verification tasks according to statistics shown in Bridge and in its own log, but this does not actually happen. There are just several active task workers that may occupy little memory thanks to speculative scheduling (according to a process table). This can result in rather inefficient usage of computational resources.