kind2 v2.0.0-7-gdcc7f6f



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

<Success> Property always_false[l186c26].timeab[l169c30].assume[l114c2] is valid by property directed reachability (IA) after 0.546s.

<Success> Property always_false[l185c22].timeab[l169c30].timeab_tmp[l119c17].assume[l99c2] is valid by inductive step after 0.629s.

<Success> Property always_false[l185c22].timeab[l169c30].timeab_exp[l115c19].assume[l86c5] is valid by inductive step after 0.629s.

<Success> Property always_false[l185c22].timeab[l169c30].assume[l114c2] is valid by inductive step after 0.629s.

<Success> Property always_false[l186c26].timeab[l169c30].timeab_tmp[l119c17].assume[l99c2] is valid by inductive step after 0.629s.

<Success> Property always_false[l186c26].timeab[l169c30].timeab_exp[l115c19].assume[l86c5] is valid by inductive step after 0.629s.

<Success> Property always_false[l186c26].timeab[l169c30].timeab_tmp[l119c17].guarantee[l101c2] is valid by 2-induction after 0.675s.

<Success> Property always_false[l185c22].timeab[l169c30].timeab_tmp[l119c17].guarantee[l101c2] is valid by 2-induction after 0.675s.

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

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

<Success> Property always_false[l185c22].timeab[l169c30].guarantee[l115c2] is valid by 2-induction after 10.727s.

<Success> Property always_false[l186c26].timeab[l169c30].guarantee[l115c2] is valid by 2-induction after 10.727s.

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

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l178c5]: valid (k=1)
guarantee[l179c5]: valid (k=1)
always_false[l185c22].timeab[l169c30].guarantee[l115c2]: valid (k=1)
always_false[l185c22].timeab[l169c30].timeab_tmp[l119c17].assume[l99c2]: valid (k=1)
always_false[l185c22].timeab[l169c30].timeab_tmp[l119c17].guarantee[l101c2]: valid (k=1)
always_false[l185c22].timeab[l169c30].timeab_exp[l115c19].assume[l86c5]: valid (k=1)
always_false[l185c22].timeab[l169c30].assume[l114c2]: valid (k=1)
always_false[l186c26].timeab[l169c30].guarantee[l115c2]: valid (k=1)
always_false[l186c26].timeab[l169c30].timeab_tmp[l119c17].assume[l99c2]: valid (k=1)
always_false[l186c26].timeab[l169c30].timeab_tmp[l119c17].guarantee[l101c2]: valid (k=1)
always_false[l186c26].timeab[l169c30].timeab_exp[l115c19].assume[l86c5]: valid (k=1)
always_false[l186c26].timeab[l169c30].assume[l114c2]: valid (k=1)
====================================================================================================================