kind2 v2.0.0-7-gdcc7f6f



====================================================================================================================
Analyzing proof_ev_true
  with First top: 'proof_ev_true'
             subsystems
               | concrete: timeab_tmp, timeab_exp, timeab, min, exist, eventually_true, P_at_k

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

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

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

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

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

<Success> Property eventually_true[l157c20].timeab[l141c28].assume[l110c2] is valid by 2-induction after 0.545s.

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

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

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

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

<Success> Property eventually_true[l158c24].timeab[l141c28].guarantee[l111c2] is valid by 2-induction after 10.728s.

<Success> Property eventually_true[l157c20].timeab[l141c28].guarantee[l111c2] is valid by 2-induction after 10.728s.

<Success> Property guarantee[l150c4] is valid by inductive step after 12.949s.

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

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l150c4]: valid (k=3)
guarantee[l151c4]: valid (k=3)
eventually_true[l157c20].assume[l127c3]: valid (k=1)
eventually_true[l157c20].timeab[l141c28].guarantee[l111c2]: valid (k=1)
eventually_true[l157c20].timeab[l141c28].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
eventually_true[l157c20].timeab[l141c28].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
eventually_true[l157c20].timeab[l141c28].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
eventually_true[l157c20].timeab[l141c28].assume[l110c2]: valid (k=1)
eventually_true[l158c24].assume[l127c3]: valid (k=1)
eventually_true[l158c24].timeab[l141c28].guarantee[l111c2]: valid (k=1)
eventually_true[l158c24].timeab[l141c28].timeab_tmp[l115c17].assume[l95c2]: valid (k=1)
eventually_true[l158c24].timeab[l141c28].timeab_tmp[l115c17].guarantee[l97c2]: valid (k=1)
eventually_true[l158c24].timeab[l141c28].timeab_exp[l111c19].assume[l82c5]: valid (k=1)
eventually_true[l158c24].timeab[l141c28].assume[l110c2]: valid (k=1)
====================================================================================================================