kind2 v2.0.0-7-gdcc7f6f



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

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

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

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

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

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

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

----------------------------------------------------------------------------------------------------------------------------------------------------------
Summary of properties:
----------------------------------------------------------------------------------------------------------------------------------------------------------
guarantee[l231c5]: valid (k=2)
guarantee[l232c5]: valid (k=2)
timeab[l264c15].assume[l117c2]: valid (k=1)
timeab[l264c47].assume[l117c2]: valid (k=1)
timeab[l257c34].assume[l117c2]: valid (k=1)
==========================================================================================================================================================