kind2 v2.0.0-7-gdcc7f6f



==========================================================================================================================================================
Analyzing proof_until_true
  with First top: 'proof_until_true'
             subsystems
               | concrete: until_true, timeab_tmp, timeab_exp, timeab, min, forall_a, exist, P_at_k

<Success> Property timeab[l188c36].assume[l117c2] is valid by property directed reachability (IA) after 0.568s.

<Success> Property timeab[l193c36].assume[l117c2] is valid by inductive step after 0.606s.

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

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

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

----------------------------------------------------------------------------------------------------------------------------------------------------------
Summary of properties:
----------------------------------------------------------------------------------------------------------------------------------------------------------
guarantee[l164c5]: valid (k=2)
guarantee[l165c5]: valid (k=2)
guarantee[l166c5]: valid (k=2)
timeab[l193c36].assume[l117c2]: valid (k=1)
timeab[l188c36].assume[l117c2]: valid (k=1)
==========================================================================================================================================================