kind2 v2.0.0-7-gdcc7f6f



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

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

<Success> Property always_true[l210c23].timeab[l137c17].timeab_tmp[l119c17].assume[l99c2] is valid by inductive step after 0.461s.

<Success> Property always_true[l210c23].timeab[l137c17].timeab_exp[l115c19].assume[l86c5] is valid by inductive step after 0.461s.

<Success> Property always_true[l210c23].timeab[l137c17].assume[l114c2] is valid by inductive step after 0.461s.

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

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

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

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

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

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

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

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l207c3]: valid (k=1)
always_true[l210c23].timeab[l137c17].guarantee[l115c2]: valid (k=1)
always_true[l210c23].timeab[l137c17].timeab_tmp[l119c17].assume[l99c2]: valid (k=1)
always_true[l210c23].timeab[l137c17].timeab_tmp[l119c17].guarantee[l101c2]: valid (k=1)
always_true[l210c23].timeab[l137c17].timeab_exp[l115c19].assume[l86c5]: valid (k=1)
always_true[l210c23].timeab[l137c17].assume[l114c2]: valid (k=1)
always_false[l211c24].timeab[l169c30].guarantee[l115c2]: valid (k=1)
always_false[l211c24].timeab[l169c30].timeab_tmp[l119c17].assume[l99c2]: valid (k=1)
always_false[l211c24].timeab[l169c30].timeab_tmp[l119c17].guarantee[l101c2]: valid (k=1)
always_false[l211c24].timeab[l169c30].timeab_exp[l115c19].assume[l86c5]: valid (k=1)
always_false[l211c24].timeab[l169c30].assume[l114c2]: valid (k=1)
====================================================================================================================