kind2 v2.0.0-7-gdcc7f6f



====================================================================================================================
Analyzing eventually_3v
  with First top: 'eventually_3v'
             subsystems
               | concrete: timeab_tmp, timeab_exp, timeab, min, forall_a, exist, eventually_true, eventually_false

<Success> Property eventually_true[l241c22].timeab[l141c28].assume[l110c2] is valid by property directed reachability (IA) after 0.602s.

<Success> Property eventually_true[l241c22].timeab[l141c28].timeab_exp[l111c19].assume[l82c5] is valid by 2-induction after 0.730s.

<Success> Property eventually_true[l241c22].timeab[l141c28].timeab_tmp[l115c17].guarantee[l97c2] is valid by 2-induction after 0.730s.

<Success> Property eventually_true[l241c22].timeab[l141c28].timeab_tmp[l115c17].assume[l95c2] is valid by 2-induction after 0.730s.

<Success> Property eventually_true[l241c22].assume[l127c3] is valid by 2-induction after 0.730s.

<Success> Property eventually_false[l246c31].timeab[l203c16].assume[l110c2] is valid by 2-induction after 0.730s.

<Success> Property eventually_false[l246c31].timeab[l203c16].timeab_exp[l111c19].assume[l82c5] is valid by 2-induction after 0.730s.

<Success> Property eventually_false[l246c31].timeab[l203c16].timeab_tmp[l115c17].guarantee[l97c2] is valid by 2-induction after 0.730s.

<Success> Property eventually_false[l246c31].timeab[l203c16].timeab_tmp[l115c17].assume[l95c2] is valid by 2-induction after 0.730s.

<Success> Property timeab[l257c21].timeab_tmp[l115c17].assume[l95c2] is valid by 2-induction after 0.730s.

<Success> Property timeab[l257c21].timeab_tmp[l115c17].guarantee[l97c2] is valid by 2-induction after 0.730s.

<Success> Property timeab[l257c21].timeab_exp[l111c19].assume[l82c5] is valid by 2-induction after 0.730s.

<Success> Property timeab[l257c21].assume[l110c2] is valid by 2-induction after 0.730s.

<Success> Property guarantee[l249c3] is valid by 2-induction after 0.730s.

<Success> Property guarantee[l245c3] is valid by 2-induction after 11.520s.

<Success> Property guarantee[l246c3] is valid by property directed reachability (QE) after 17.837s.

<Success> Property timeab[l257c21].guarantee[l111c2] is valid by property directed reachability (QE) after 17.837s.

<Success> Property eventually_false[l246c31].timeab[l203c16].guarantee[l111c2] is valid by property directed reachability (QE) after 17.837s.

<Success> Property eventually_true[l241c22].timeab[l141c28].guarantee[l111c2] is valid by property directed reachability (QE) after 17.837s.

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l245c3]: valid (k=1)
guarantee[l246c3]: valid (k=1)
guarantee[l249c3]: valid (k=1)
timeab[l257c21].assume[l110c2]: valid (k=1)
timeab[l257c21].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
timeab[l257c21].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
timeab[l257c21].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
timeab[l257c21].guarantee[l111c2]: valid (k=1)
eventually_false[l246c31].timeab[l203c16].guarantee[l111c2]: valid (k=1)
eventually_false[l246c31].timeab[l203c16].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
eventually_false[l246c31].timeab[l203c16].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
eventually_false[l246c31].timeab[l203c16].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
eventually_false[l246c31].timeab[l203c16].assume[l110c2]: valid (k=1)
eventually_true[l241c22].assume[l127c3]: valid (k=1)
eventually_true[l241c22].timeab[l141c28].guarantee[l111c2]: valid (k=1)
eventually_true[l241c22].timeab[l141c28].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
eventually_true[l241c22].timeab[l141c28].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
eventually_true[l241c22].timeab[l141c28].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
eventually_true[l241c22].timeab[l141c28].assume[l110c2]: valid (k=1)
====================================================================================================================