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) ====================================================================================================================