kind2 v2.0.0-7-gdcc7f6f



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

<Success> Property always_true[l153c25].timeab[l137c17].assume[l114c2] is valid by property directed reachability (IA) after 0.800s.

<Success> Property always_true[l153c25].timeab[l137c17].timeab_exp[l115c19].assume[l86c5] is valid by 2-induction after 0.871s.

<Success> Property always_true[l153c25].timeab[l137c17].timeab_tmp[l119c17].guarantee[l101c2] is valid by 2-induction after 0.871s.

<Success> Property always_true[l153c25].timeab[l137c17].timeab_tmp[l119c17].assume[l99c2] is valid by 2-induction after 0.871s.

<Success> Property always_true[l152c21].timeab[l137c17].assume[l114c2] is valid by 2-induction after 0.871s.

<Success> Property always_true[l152c21].timeab[l137c17].timeab_exp[l115c19].assume[l86c5] is valid by 2-induction after 0.871s.

<Success> Property always_true[l152c21].timeab[l137c17].timeab_tmp[l119c17].guarantee[l101c2] is valid by 2-induction after 0.871s.

<Success> Property always_true[l152c21].timeab[l137c17].timeab_tmp[l119c17].assume[l99c2] is valid by 2-induction after 0.871s.

<Error> Caught exception in invariant generator: Invalid_argument("mk_const_state_var")

<Success> Property always_true[l152c21].timeab[l137c17].guarantee[l115c2] is valid by 2-induction after 26.719s.

<Success> Property always_true[l153c25].timeab[l137c17].guarantee[l115c2] is valid by 2-induction after 51.492s.

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

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

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l145c4]: valid (k=1)
guarantee[l146c4]: valid (k=1)
always_true[l152c21].timeab[l137c17].guarantee[l115c2]: valid (k=1)
always_true[l152c21].timeab[l137c17].timeab_tmp[l119c17].assume[l99c2]: valid (k=1)
always_true[l152c21].timeab[l137c17].timeab_tmp[l119c17].guarantee[l101c2]: valid (k=1)
always_true[l152c21].timeab[l137c17].timeab_exp[l115c19].assume[l86c5]: valid (k=1)
always_true[l152c21].timeab[l137c17].assume[l114c2]: valid (k=1)
always_true[l153c25].timeab[l137c17].guarantee[l115c2]: valid (k=1)
always_true[l153c25].timeab[l137c17].timeab_tmp[l119c17].assume[l99c2]: valid (k=1)
always_true[l153c25].timeab[l137c17].timeab_tmp[l119c17].guarantee[l101c2]: valid (k=1)
always_true[l153c25].timeab[l137c17].timeab_exp[l115c19].assume[l86c5]: valid (k=1)
always_true[l153c25].timeab[l137c17].assume[l114c2]: valid (k=1)
====================================================================================================================