===== RandTree badRoot bug =====

In this page we describe the bug found exclusively by CrystalBall for RandTree.

==== Safety Property ====

Root must not be a member of children list.


==== live run states ====

This figure shows the live run state when consequence search got started.

{{crystalball:randtree-badroovi_mt-initial-states.gif|randtree-badRoot-initial-states.gif}}

==== Consequence search path ====

This figures depicts the bath consequence search found towards the bug.

{{crystalball:randtree-badRoot-consequence-search-path.gif|randtree-badRoot-consequence-search-path.gif}}