examples/regtests.out

   1 === Programs already ported === MUST REPLAY AND ALL GOALS PROVED ===
   2
   3 Replaying ./add_list_vc_sp ... OK 4/4 (replay OK)
   4 Replaying ./add_list ... OK 4/4 (replay OK)
   5 Replaying ./algo63 ... OK 3/3 (replay OK)
   6 Replaying ./algo64 ... OK 2/2 (replay OK)
   7 Replaying ./algo65 ... OK 1/1 (replay OK)
   8 Replaying ./all_distinct ... OK 1/1 (replay OK)
   9 Replaying ./amortization ... OK 2/2 (replay OK)
  10 Replaying ./arm ... OK 3/3 (replay OK)
  11 Replaying ./array_most_frequent ... OK 1/1 (replay OK)
  12 Replaying ./assigning_meanings_to_programs ... OK 2/2 (replay OK)
  13 Replaying ./bag ... OK 13/13 (replay OK)
  14 Replaying ./balance ... OK 3/3 (replay OK)
  15 Replaying ./bellman_ford ... OK 11/11 (replay OK)
  16 Replaying ./bignum ... OK 5/5 (replay OK)
  17 Replaying ./binary_multiplication ... OK 2/2 (replay OK)
  18 Replaying ./binary_search_vc_sp ... OK 4/4 (replay OK)
  19 Replaying ./binary_search ... OK 9/9 (replay OK)
  20 Replaying ./binary_sort ... OK 2/2 (replay OK)
  21 Replaying ./binary_sqrt ... OK 2/2 (replay OK)
  22 Replaying ./binomial_heap ... OK 23/23 (replay OK)
  23 Replaying ./bitcount ... OK 25/25 (replay OK)
  24 Replaying ./bitvector_examples ... OK 86/86 (replay OK)
  25 Replaying ./bitwalker ... OK 14/14 (replay OK)
  26 Replaying ./braun_trees ... OK 12/12 (replay OK)
  27 Replaying ./bresenham ... OK 2/2 (replay OK)
  28 Replaying ./bubble_sort ... OK 4/4 (replay OK)
  29 Replaying ./checking_a_large_routine ... OK 2/2 (replay OK)
  30 Replaying ./coincidence_count_list ... OK 7/7 (replay OK)
  31 Replaying ./coincidence_count ... OK 9/9 (replay OK)
  32 Replaying ./conjugate ... OK 4/4 (replay OK)
  33 Replaying ./counting_sort ... OK 4/4 (replay OK)
  34 Replaying ./cubic_root ... OK 1/1 (replay OK)
  35 Replaying ./cursor_examples ... OK 26/26 (replay OK)
  36 Replaying ./decrease1 ... OK 3/3 (replay OK)
  37 Replaying ./defunctionalization ... OK 43/43 (replay OK)
  38 Replaying ./dfa_example ... OK 10/10 (replay OK)
  39 Replaying ./dfs ... OK 4/4 (replay OK)
  40 Replaying ./dijkstra ... OK 8/8 (replay OK)
  41 Replaying ./disamb ... OK 10/10 (replay OK)
  42 Replaying ./division ... OK 11/11 (replay OK)
  43 Replaying ./dyck ... OK 4/4 (replay OK)
  44 Replaying ./edit_distance ... OK 13/13 (replay OK)
  45 Replaying ./equality_up_to_spaces ... OK 2/2 (replay OK)
  46 Replaying ./esterel ... OK 5/5 (replay OK)
  47 Replaying ./euler001 ... OK 28/28 (replay OK)
  48 Replaying ./euler002 ... OK 6/6 (replay OK)
  49 Replaying ./euler011 ... OK 5/5 (replay OK)
  50 Replaying ./euler_sieve ... OK 45/45 (replay OK)
  51 Replaying ./ewd673 ... OK 1/1 (replay OK)
  52 Replaying ./fact_vc_sp ... OK 10/10 (replay OK)
  53 Replaying ./fact ... OK 10/10 (replay OK)
  54 Replaying ./fenwick ... OK 5/5 (replay OK)
  55 Replaying ./fib_memo ... OK 2/2 (replay OK)
  56 Replaying ./fibonacci ... OK 27/27 (replay OK)
  57 Replaying ./fill ... OK 1/1 (replay OK)
  58 Replaying ./find ... OK 1/1 (replay OK, obsolete session)
  59 [Warning] session is obsolete
  60 Replaying ./finger_trees ... OK 3/3 (replay OK)
  61 Replaying ./finite_tarski ... OK 2/2 (replay OK)
  62 Replaying ./flag2 ... OK 12/12 (replay OK)
  63 Replaying ./flag ... OK 1/1 (replay OK)
  64 Replaying ./foveoos11_challenge1 ... OK 1/1 (replay OK)
  65 Replaying ./foveoos11_challenge2 ... OK 2/2 (replay OK)
  66 Replaying ./foveoos11_challenge3 ... OK 1/1 (replay OK)
  67 Replaying ./f_puzzle ... OK 9/9 (replay OK)
  68 Replaying ./gcd_bezout_vc_sp ... OK 1/1 (replay OK, obsolete session)
  69 [Warning] session is obsolete
  70 Replaying ./gcd_bezout ... OK 1/1 (replay OK)
  71 Replaying ./gcd_vc_sp ... OK 13/13 (replay OK)
  72 Replaying ./gcd ... OK 13/13 (replay OK)
  73 Replaying ./generate_all_trees ... OK 6/6 (replay OK)
  74 Replaying ./gnome_sort ... OK 1/1 (replay OK)
  75 Replaying ./hackers-delight ... OK 51/51 (replay OK)
  76 Replaying ./hashtbl_impl ... OK 11/11 (replay OK)
  77 Replaying ./hillel_challenge ... OK 11/11 (replay OK)
  78 Replaying ./huffman_with_two_queues ... OK 4/4 (replay OK)
  79 Replaying ./induction ... OK 10/10 (replay OK)
  80 Replaying ./infinity_of_primes ... OK 2/2 (replay OK)
  81 Replaying ./insertion_sort_list ... OK 3/3 (replay OK)
  82 Replaying ./insertion_sort_naive ... OK 4/4 (replay OK)
  83 Replaying ./insertion_sort ... OK 6/6 (replay OK)
  84 Replaying ./inverse_in_place ... OK 4/4 (replay OK)
  85 Replaying ./isqrt_von_neumann ... OK 6/6 (replay OK)
  86 Replaying ./isqrt ... OK 6/6 (replay OK)
  87 Replaying ./kleene_algebra ... OK 83/83 (replay OK)
  88 Replaying ./kmp ... OK 13/13 (replay OK)
  89 Replaying ./knuth_prime_numbers ... OK 3/3 (replay OK)
  90 Replaying ./koda_ruskey ... OK 40/40 (replay OK)
  91 Replaying ./largest_prime_factor ... OK 4/4 (replay OK)
  92 Replaying ./lcp ... OK 2/2 (replay OK)
  93 Replaying ./leftist_heap ... OK 13/13 (replay OK)
  94 Replaying ./linear_probing ... OK 16/16 (replay OK)
  95 Replaying ./linked_list_rev ... OK 22/22 (replay OK)
  96 Replaying ./list_removal ... OK 8/8 (replay OK)
  97 Replaying ./maximum_subarray ... OK 7/7 (replay OK)
  98 Replaying ./max_matrix ... OK 4/4 (replay OK)
  99 Replaying ./mccarthy_vc_sp ... OK 6/6 (replay OK)
 100 Replaying ./mccarthy ... OK 11/11 (replay OK)
 101 Replaying ./mergesort_array ... OK 9/9 (replay OK, obsolete session)
 102 [Warning] session is obsolete
 103 Replaying ./mergesort_list ... OK 20/20 (replay OK)
 104 Replaying ./mergesort_queue ... OK 5/5 (replay OK)
 105 Replaying ./mex ... OK 2/2 (replay OK)
 106 Replaying ./min_max ... OK 4/4 (replay OK)
 107 Replaying ./mjrty ... OK 1/1 (replay OK)
 108 Replaying ./muller ... OK 1/1 (replay OK)
 109 Replaying ./mutual_recursion ... OK 4/4 (replay OK)
 110 Replaying ./my_cosine ... FAILED (ret code=1): 1/1 (replay failed)
 111    goal 'my_cosine'vc.0', prover 'Coq 8.9.1': High failure (0.29s),
 112                                               Prover exit status: exited with status 1
 113                                               prover output:
 114                                               File "/tmp/why_48a7c6_my_cosine_T_my_cosineqtvc.v", line 136, characters 15-39:
 115 Error:
 116 Cannot find a physical path bound to logical path matching suffix Interval.
 117
 118
 119                                                instead of Valid (1.61s) (timelimit=5, memlimit=1000, steplimit=0)
 120 Replaying ./nistonacci ... OK 4/4 (replay OK)
 121 Replaying ./optimal_replay ... OK 1/1 (replay OK)
 122 Replaying ./pairing_heap_bin ... OK 16/16 (replay OK)
 123 Replaying ./pairing_heap ... OK 31/31 (replay OK)
 124 Replaying ./pancake_sorting ... OK 2/2 (replay OK)
 125 Replaying ./patience ... OK 8/8 (replay OK)
 126 Replaying ./pigeonhole ... OK 2/2 (replay OK)
 127 Replaying ./power_vc_sp ... OK 2/2 (replay OK)
 128 Replaying ./power ... OK 2/2 (replay OK)
 129 Replaying ./queens_bv ... OK 16/16 (replay OK, obsolete session)
 130 [Warning] session is obsolete
 131 Replaying ./queens ... OK 5/5 (replay OK, obsolete session)
 132 [Warning] session is obsolete
 133 Replaying ./queue_two_lists ... OK 25/25 (replay OK)
 134 Replaying ./quicksort ... OK 12/12 (replay OK)
 135 Replaying ./random_access_list ... OK 20/20 (replay OK)
 136 Replaying ./register_allocation ... OK 12/12 (replay OK)
 137 Replaying ./relabel ... OK 4/4 (replay OK)
 138 Replaying ./remove_duplicate_hash ... OK 1/1 (replay OK)
 139 Replaying ./remove_duplicate ... OK 2/2 (replay OK)
 140 Replaying ./residual ... OK 5/5 (replay OK)
 141 Replaying ./resizable_array ... OK 8/8 (replay OK)
 142 Replaying ./rightmostbittrick ... OK 2/2 (replay OK)
 143 Replaying ./ring_buffer ... OK 4/4 (replay OK)
 144 Replaying ./ropes ... OK 17/17 (replay OK)
 145 Replaying ./same_fringe ... OK 3/3 (replay OK)
 146 Replaying ./schorr_waite_via_recursion ... OK 2/2 (replay OK, obsolete session)
 147 [Warning] session is obsolete
 148 Replaying ./schorr_waite ... OK 7/7 (replay OK)
 149 Replaying ./schorr_waite_with_ghost_monitor ... OK 1/1 (replay OK)
 150 Replaying ./selection_sort ... OK 4/4 (replay OK)
 151 Replaying ./sf ... OK 10/10 (replay OK)
 152 Replaying ./sieve ... OK 2/2 (replay OK)
 153 Replaying ./skew_heaps ... OK 7/7 (replay OK)
 154 Replaying ./snapshotable_trees ... OK 13/13 (replay OK)
 155 Replaying ./sorted_list ... OK 2/2 (replay OK)
 156 Replaying ./string_base64_encoding ... OK 14/14 (replay OK)
 157 Replaying ./string_hex_encoding ... OK 6/6 (replay OK)
 158 Replaying ./string_search ... OK 8/8 (replay OK)
 159 Replaying ./subsequence ... OK 1/1 (replay OK)
 160 Replaying ./sudoku ... OK 20/20 (replay OK)
 161 Replaying ./sumrange ... OK 20/20 (replay OK)
 162 Replaying ./swap ... OK 4/4 (replay OK)
 163 Replaying ./there_and_back_again ... OK 4/4 (replay OK)
 164 Replaying ./three_idem_ring ... OK 27/27 (replay OK)
 165 Replaying ./topological_sorting ... OK 5/5 (replay OK)
 166 Replaying ./tortoise_and_hare ... OK 4/4 (replay OK)
 167 Replaying ./tower_of_hanoi ... OK 9/9 (replay OK)
 168 Replaying ./toy_compiler ... OK 2/2 (replay OK)
 169 Replaying ./tree_height ... OK 11/11 (replay OK)
 170 Replaying ./tree_of_array ... OK 2/2 (replay OK)
 171 Replaying ./tree_of_list ... OK 2/2 (replay OK)
 172 Replaying ./unraveling_a_card_trick ... OK 5/5 (replay OK)
 173 Replaying ./vacid_0_build_maze ... OK 3/3 (replay OK)
 174 Replaying ./vacid_0_red_black_trees ... OK 37/37 (replay OK)
 175 Replaying ./vacid_0_sparse_array ... OK 8/8 (replay OK)
 176 Replaying ./verifythis_2015_dancing_links ... OK 3/3 (replay OK)
 177 Replaying ./verifythis_2015_parallel_gcd ... OK 6/6 (replay OK)
 178 Replaying ./verifythis_2015_relaxed_prefix ... OK 1/1 (replay OK)
 179 Replaying ./verifythis_2016_tree_traversal ... OK 10/10 (replay OK)
 180 Replaying ./verifythis_2017_maximum_sum_submatrix ... OK 1/1 (replay OK)
 181 Replaying ./verifythis_2017_odd_even_sort_rearranging ... OK 8/8 (replay OK)
 182 Replaying ./verifythis_2017_odd_even_transposition_sort ... OK 2/2 (replay OK)
 183 Replaying ./verifythis_2017_pair_insertion_sort ... OK 1/1 (replay OK)
 184 Replaying ./verifythis_2017_tree_buffer ... OK 10/10 (replay OK)
 185 Replaying ./verifythis_2018_array_based_queuing_lock_1 ... OK 8/8 (replay OK)
 186 Replaying ./verifythis_2018_array_based_queuing_lock_2 ... OK 10/10 (replay OK, obsolete session)
 187 [Warning] session is obsolete
 188 Replaying ./verifythis_2018_le_rouge_et_le_noir_1 ... OK 23/23 (replay OK, obsolete session)
 189 [Warning] session is obsolete
 190 Replaying ./verifythis_2018_le_rouge_et_le_noir_2 ... OK 8/8 (replay OK)
 191 Replaying ./verifythis_2018_mind_the_gap_1 ... OK 6/6 (replay OK)
 192 Replaying ./verifythis_2018_mind_the_gap_2 ... OK 6/6 (replay OK)
 193 Replaying ./verifythis_2018_register_allocation ... OK 10/10 (replay OK)
 194 Replaying ./verifythis_2019_cartesian_trees ... OK 15/15 (replay OK)
 195 Replaying ./verifythis_2019_ghc_sort ... OK 24/24 (replay OK, obsolete session)
 196 [Warning] session is obsolete
 197 Replaying ./verifythis_2021_dll_to_bst ... OKSymbol '([])'result'unused'unused' not found, ignored
 198 Symbol '(=)'result'unused'unused' not found, ignored
 199 Symbol '([])'result'unused'unused' not found, ignored
 200 Symbol '(=)'result'unused'unused' not found, ignored
 201 Symbol '([])'result'unused'unused' not found, ignored
 202 Symbol '(=)'result'unused'unused' not found, ignored
 203 Symbol '([])'result'unused'unused' not found, ignored
 204 Symbol '(=)'result'unused'unused' not found, ignored
 205 Symbol '([])'result'unused'unused' not found, ignored
 206 Symbol '(=)'result'unused'unused' not found, ignored
 207 Symbol '([])'result'unused'unused' not found, ignored
 208 Symbol '(=)'result'unused'unused' not found, ignored
 209  10/10 (replay OK)
 210 Replaying ./verifythis_2021_lexicographic_permutations_1 ... OK 17/17 (replay OK)
 211 Replaying ./verifythis_2021_lexicographic_permutations_2 ... OK 27/27 (replay OK, obsolete session)
 212 [Warning] session is obsolete
 213 Replaying ./verifythis_2021_shearsort_modified ... OK 2/2 (replay OK)
 214 Replaying ./verifythis_2021_shearsort ... OKFile "/users/vals/bbecker/why3/examples/./verifythis_2021_shearsort.mlw", line 679, characters 8-17: cloned theory .ShearSort does not contain any abstract symbol; it should be used instead
 215  12/12 (replay OK)
 216 Replaying ./verifythis_fm2012_LRS ... OK 20/20 (replay OK)
 217 Replaying ./verifythis_fm2012_treedel ... OK 12/12 (replay OK)
 218 Replaying ./verifythis_PrefixSumRec ... OK 9/9 (replay OK)
 219 Replaying ./vstte10_aqueue ... OK 6/6 (replay OK)
 220 Replaying ./vstte10_inverting ... OK 3/3 (replay OK)
 221 Replaying ./vstte10_max_sum ... OK 3/3 (replay OK)
 222 Replaying ./vstte10_queens ... OK 17/17 (replay OK)
 223 Replaying ./vstte10_search_list ... OK 5/5 (replay OK)
 224 Replaying ./vstte12_bfs ... OK 6/6 (replay OK)
 225 Replaying ./vstte12_combinators ... OK 12/12 (replay OK)
 226 Replaying ./vstte12_ring_buffer ... OK 20/20 (replay OK)
 227 Replaying ./vstte12_tree_reconstruction ... OK 23/23 (replay OK)
 228 Replaying ./vstte12_two_way_sort ... OK 1/1 (replay OK)
 229 Replaying ./warshall_algorithm ... OK 3/3 (replay OK)
 230 Replaying ./white_and_black_balls ... OK 1/1 (replay OK)
 231 Replaying ./word_common_factor ... OK 3/3 (replay OK)
 232 Replaying ./wrap_lines ... OK 6/6 (replay OK)
 233 Replaying ./zeros ... OK 7/7 (replay OK)
 234 Replaying micro-c/dicho ... OK 2/2 (replay OK)
 235 Replaying micro-c/isqrt ... OK 1/1 (replay OK)
 236 Replaying micro-c/loops ... OK 2/2 (replay OK)
 237 Replaying micro-c/mult ... OK 1/1 (replay OK)
 238 Replaying micro-c/sort ... OK 2/2 (replay OK)
 239 Replaying micro-c/triangular ... OK 3/3 (replay OK)
 240 Replaying python/arrays ... OK 1/1 (replay OK)
 241 Replaying python/break_continue ... OK 1/1 (replay OK)
 242 Replaying python/check_duplicates ... OK 1/1 (replay OK)
 243 Replaying python/concat ... OK 1/1 (replay OK)
 244 Replaying python/dicho ... OK 1/1 (replay OK)
 245 Replaying python/even ... OK 1/1 (replay OK)
 246 Replaying python/fact ... OK 1/1 (replay OK)
 247 Replaying python/isqrt_fun ... OK 1/1 (replay OK)
 248 Replaying python/isqrt ... OK 1/1 (replay OK)
 249 Replaying python/is_sorted ... OK 1/1 (replay OK)
 250 Replaying python/mult ... OK 1/1 (replay OK)
 251 Replaying python/nim ... OK 1/1 (replay OK)
 252 Replaying python/pgcd ... OK 1/1 (replay OK)
 253 Replaying python/range ... OK 1/1 (replay OK)
 254 Replaying python/reverse ... OK 1/1 (replay OK)
 255 Replaying python/sort ... OK 1/1 (replay OK)
 256 Replaying python/sum_reverse ... OK 1/1 (replay OK)
 257 Replaying python/triangular ... OK 1/1 (replay OK)
 258 Replaying double_wp/compiler ... OK 9/9 (replay OK)
 259 Replaying double_wp/imp ... OK 2/2 (replay OK)
 260 Replaying double_wp/logic ... OK 12/12 (replay OK)
 261 Replaying double_wp/specs ... OK 15/15 (replay OK)
 262 Replaying double_wp/state ... OK 0/0 (replay OK)
 263 Replaying double_wp/vm ... OK 4/4 (replay OK)
 264 Replaying avl/avl ... OK 31/31 (replay OK)
 265 Replaying avl/key_type ... OK 0/0 (replay OK)
 266 Replaying avl/monoid ... OK 8/8 (replay OK)
 267 Replaying avl/preorder ... OK 7/7 (replay OK)
 268 Replaying avl/priority_queue ... OK 34/34 (replay OK)
 269 Replaying avl/ral ... OK 37/37 (replay OK)
 270 Replaying avl/tables ... OK 106/106 (replay OK)
 271 Replaying c_cursor/ccursor ... OK 5/5 (replay OK)
 272 Replaying foveoos11-cm/array_max ... OK 1/1 (replay OK)
 273 Replaying foveoos11-cm/duplets ... OK 2/2 (replay OK)
 274 Replaying foveoos11-cm/tree_max ... OK 3/3 (replay OK)
 275 Replaying vacid_0_binary_heaps/proofs ... OK 38/38 (replay OK)
 276 Replaying verifythis_2016_matrix_multiplication/matrices_ring_simp ... OK 23/23 (replay OK)
 277 Replaying verifythis_2016_matrix_multiplication/matrices ... OK 23/23 (replay OK)
 278 Replaying verifythis_2016_matrix_multiplication/naive ... OK 1/1 (replay OK)
 279 Replaying verifythis_2016_matrix_multiplication/strassen ... OK 14/14 (replay OK)
 280 Replaying verifythis_2016_matrix_multiplication/sum_extended ... OK 4/4 (replay OK)
 281 Replaying WP_revisited/blocking_semantics5 ... OK 38/38 (replay OK)
 282 Replaying WP_revisited/formula ... OK 1/1 (replay OK)
 283 Replaying WP_revisited/imp_n ... OK 18/18 (replay OK)
 284 Replaying WP_revisited/wp2 ... OK 30/30 (replay OK)
 285 Replaying prover/BacktrackArray ... OK 8/8 (replay OK)
 286 Replaying prover/Choice ... OK 0/0 (replay OK)
 287 Replaying prover/Firstorder_formula_impl ... OK 16/16 (replay OK)
 288 Replaying prover/Firstorder_formula_list_impl ... OK 16/16 (replay OK)
 289 Replaying prover/Firstorder_formula_list_spec ... OK 25/25 (replay OK)
 290 Replaying prover/Firstorder_formula_spec ... OK 25/25 (replay OK)
 291 Replaying prover/Firstorder_semantics ... OK 24/24 (replay OK)
 292 Replaying prover/Firstorder_symbol_impl ... OK 12/12 (replay OK)
 293 Replaying prover/Firstorder_symbol_spec ... OK 32/32 (replay OK)
 294 Replaying prover/Firstorder_tableau_impl ... OK 16/16 (replay OK)
 295 Replaying prover/Firstorder_tableau_spec ... OK 25/25 (replay OK)
 296 Replaying prover/Firstorder_term_impl ... OK 33/33 (replay OK)
 297 Replaying prover/Firstorder_term_spec ... OK 64/64 (replay OK)
 298 Replaying prover/FormulaTransformations ... OK 27/27 (replay OK)
 299 Replaying prover/Functions ... OK 6/6 (replay OK)
 300 Replaying prover/ISet ... OK 4/4 (replay OK)
 301 Replaying prover/Nat ... OK 3/3 (replay OK)
 302 Replaying prover/OptionFuncs ... OK 12/12 (replay OK)
 303 Replaying prover/Predicates ... OK 4/4 (replay OK)
 304 Replaying prover/ProverMain ... OK 1/1 (replay OK)
 305 Replaying prover/ProverTest ... OK 14/14 (replay OK)
 306 Replaying prover/Prover ... OK 16/16 (replay OK)
 307 Replaying prover/Sum ... OK 0/0 (replay OK)
 308 Replaying prover/Unification ... OK 11/11 (replay OK)
 309 Replaying multiprecision/add_1 ... OK 4/4 (replay OK)
 310 Replaying multiprecision/add ... OK 12/12 (replay OK, obsolete session)
 311 [Warning] session is obsolete
 312 Replaying multiprecision/base_info ... OK 5/5 (replay OK)
 313 Replaying multiprecision/compare ... OK 1/1 (replay OK)
 314 Replaying multiprecision/div ... OK 13/13 (replay OK, obsolete session)
 315 [Warning] session is obsolete
 316 Replaying multiprecision/get_str ... OK 4/4 (replay OK, obsolete session)
 317 [Warning] session is obsolete
 318 Replaying multiprecision/lemmas ... OK 25/25 (replay OK)
 319 Replaying multiprecision/lineardecision ... OK 226/226 (replay OK)
 320 Replaying multiprecision/logical ... OK 13/13 (replay OK, obsolete session)
 321 [Warning] session is obsolete
 322 Replaying multiprecision/mpz_abs ... OK 1/1 (replay OK)
 323 Replaying multiprecision/mpz_add ... OK 2/2 (replay OK)
 324 Replaying multiprecision/mpz_cmpabs ... OK 3/3 (replay OK)
 325 Replaying multiprecision/mpz_cmp ... OK 4/4 (replay OK)
 326 Replaying multiprecision/mpz_div2exp ... OK 3/3 (replay OK)
 327 Replaying multiprecision/mpz_div ... OK 2/2 (replay OK, obsolete session)
 328 [Warning] session is obsolete
 329 Replaying multiprecision/mpz_getset ... OK 4/4 (replay OK)
 330 Replaying multiprecision/mpz_get_str ... OK 3/3 (replay OK)
 331 Replaying multiprecision/mpz_mul2exp ... OK 1/1 (replay OK, obsolete session)
 332 [Warning] session is obsolete
 333 Replaying multiprecision/mpz_mul ... OK 3/3 (replay OK)
 334 Replaying multiprecision/mpz_neg ... OK 1/1 (replay OK)
 335 Replaying multiprecision/mpz_realloc2 ... OK 1/1 (replay OK)
 336 Replaying multiprecision/mpz_set_str ... OK 1/1 (replay OK)
 337 Replaying multiprecision/mpz_sub ... OK 3/3 (replay OK)
 338 Replaying multiprecision/mpz ... OK 9/9 (replay OK)
 339 Replaying multiprecision/mul ... OK 7/7 (replay OK, obsolete session)
 340 [Warning] session is obsolete
 341 Replaying multiprecision/powm ... OK 18/18 (replay OK, obsolete session)
 342 [Warning] session is obsolete
 343 Replaying multiprecision/set_str ... OK 3/3 (replay OK, obsolete session)
 344 [Warning] session is obsolete
 345 Replaying multiprecision/sqrtrem ... OK 6/6 (replay OK, obsolete session)
 346 [Warning] session is obsolete
 347 Replaying multiprecision/sqrt ... OK 3/3 (replay OK)
 348 Replaying multiprecision/stringlemmas ... OK 40/40 (replay OK)
 349 Replaying multiprecision/sub_1 ... OK 4/4 (replay OK)
 350 Replaying multiprecision/sub ... OK 12/12 (replay OK, obsolete session)
 351 [Warning] session is obsolete
 352 Replaying multiprecision/toom ... OK 8/8 (replay OK, obsolete session)
 353 [Warning] session is obsolete
 354 Replaying multiprecision/types ... OK 0/0 (replay OK)
 355 Replaying multiprecision/util ... OK 7/7 (replay OK)
 356 Replaying multiprecision/valuation ... OK 14/14 (replay OK)
 357 Replaying multiprecision/wmpn ... OK 0/0 (replay OK)
 358
 359 Score on ported programs : 310/311
 360
 361 === Standard Library ===
 362
 363 Replaying stdlib/array ... OK 22/22 (replay OK)
 364 Replaying stdlib/bintree ... OK 6/6 (replay OK)
 365 Replaying stdlib/byte_string ... OK 2/2 (replay OK)
 366 Replaying stdlib/list ... OK 54/54 (replay OK)
 367 Replaying stdlib/pigeon ... OK 4/6 (replay OK)
 368    +--file [../../../stdlib/pigeon.mlw]: 4/6
 369       +--theory ListAndSet: 3/5
 370          +--goal corner not proved
 371          +--goal pigeon_1 not proved
 372 Replaying stdlib/pqueue ... OK 5/5 (replay OK)
 373 Replaying stdlib/stringCheck ... OK 60/60 (replay OK)
 374 Replaying stdlib/tagset ... OK 14/14 (replay OK)
 375 Replaying stdlib/witness ... OK 1/1 (replay OK)
 376
 377 === Tests ===
 378
 379 Replaying tests-provers/bitvec ... OK 6/6 (replay OK)
 380 Replaying tests-provers/bv ... OK 157/198 (replay OK)
 381    +--file [../bv.why]: 157/198
 382       +--theory CheckBV64: 58/71
 383          +--goal trap not proved
 384          +--goal smoke1 not proved
 385          +--goal smoke2 not proved
 386          +--goal smoke3 not proved
 387          +--goal smoke4 not proved
 388          +--goal smoke5 not proved
 389          +--goal smoke6 not proved
 390          +--goal smoke7 not proved
 391          +--goal smoke8 not proved
 392          +--goal f1 not proved
 393          +--goal f2 not proved
 394          +--goal f3 not proved
 395          +--goal f7 not proved
 396       +--theory CheckBV32: 33/42
 397          +--goal trap not proved
 398          +--goal smoke1 not proved
 399          +--goal smoke2 not proved
 400          +--goal smoke3 not proved
 401          +--goal smoke4 not proved
 402          +--goal smoke5 not proved
 403          +--goal smoke6 not proved
 404          +--goal smoke7 not proved
 405          +--goal smoke8 not proved
 406       +--theory CheckBV16: 33/42
 407          +--goal trap not proved
 408          +--goal smoke1 not proved
 409          +--goal smoke2 not proved
 410          +--goal smoke3 not proved
 411          +--goal smoke4 not proved
 412          +--goal smoke5 not proved
 413          +--goal smoke6 not proved
 414          +--goal smoke7 not proved
 415          +--goal smoke8 not proved
 416       +--theory CheckBV8: 33/42
 417          +--goal trap not proved
 418          +--goal smoke1 not proved
 419          +--goal smoke2 not proved
 420          +--goal smoke3 not proved
 421          +--goal smoke4 not proved
 422          +--goal smoke5 not proved
 423          +--goal smoke6 not proved
 424          +--goal smoke7 not proved
 425          +--goal smoke8 not proved
 426       +--theory Extras: 0/1
 427          +--goal mod_mult not proved
 428 Replaying tests-provers/ceil ... OK 12/12 (replay OK)
 429 Replaying tests-provers/coq-interval ... FAILED (ret code=1): 0/1 (replay failed)
 430    goal 'pow_eps2_max_int', prover 'Coq 8.9.1': High failure (0.28s),
 431                                                 Prover exit status: exited with status 1
 432                                                 prover output:
 433                                                 File "/tmp/why_f8d102_coqmninterval_T_pow_eps2_max_int.v", line 11, characters 15-39:
 434 Error:
 435 Cannot find a physical path bound to logical path matching suffix Interval.
 436
 437
 438                                                  instead of Valid (0.77s) (timelimit=5, memlimit=1000, steplimit=0)
 439 Replaying tests-provers/coq ... OK 1/1 (replay OK)
 440 Replaying tests-provers/cvc3 ... OK 1/3 (replay OK)
 441    +--file [../cvc3.why]: 1/3
 442       +--theory Test: 1/3
 443          +--goal test1 not proved
 444          +--goal test2 not proved
 445 Replaying tests-provers/div_real ... OK 9/12 (replay OK)
 446    +--file [../div_real.why]: 9/12
 447       +--theory DivTest: 9/12
 448          +--goal smoke1 not proved
 449          +--goal smoke3 not proved
 450          +--goal smoke5 not proved
 451 Replaying tests-provers/div ... OK 13/25 (replay OK)
 452    +--file [../div.why]: 13/25
 453       +--theory EuclideanDivTest: 6/12
 454          +--goal smoke1 not proved
 455          +--goal smoke2 not proved
 456          +--goal smoke3 not proved
 457          +--goal smoke4 not proved
 458          +--goal smoke5 not proved
 459          +--goal smoke6 not proved
 460       +--theory ComputerDivTest: 7/13
 461          +--goal smoke1 not proved
 462          +--goal smoke2 not proved
 463          +--goal smoke3 not proved
 464          +--goal smoke4 not proved
 465          +--goal smoke5 not proved
 466          +--goal smoke6 not proved
 467 Replaying tests-provers/gappa ... OK 14/14 (replay OK)
 468 Replaying tests-provers/ieee_float ... FAILED (ret code=1): 16/20 (replay failed)
 469    goal 'wrong', prover 'Isabelle 2018': High failure (1.82s),
 470                                          Prover exit status: exited with status 2
 471                                          prover output:
 472                                          *** Unknown Isabelle tool: "why3"
 473
 474                                           instead of Unknown () (7.18s) (timelimit=0, memlimit=0, steplimit=0)
 475    goal 'ok', prover 'Isabelle 2018': High failure (1.87s),
 476                                       Prover exit status: exited with status 2
 477                                       prover output:
 478                                       *** Unknown Isabelle tool: "why3"
 479
 480                                        instead of Valid (6.95s) (timelimit=0, memlimit=0, steplimit=0)
 481    goal 'more', prover 'Isabelle 2018': High failure (1.84s),
 482                                         Prover exit status: exited with status 2
 483                                         prover output:
 484                                         *** Unknown Isabelle tool: "why3"
 485
 486                                          instead of Valid (7.22s) (timelimit=0, memlimit=0, steplimit=0)
 487 Replaying tests-provers/metitarski ... OK 5/11 (replay OK)
 488    +--file [../metitarski.why]: 5/11
 489       +--theory P3: 2/4
 490          +--goal cos_bound not proved
 491          +--goal MethodErrorWrong not proved
 492       +--theory Power: 0/3
 493          +--goal G not proved
 494          +--goal G1 not proved
 495          +--goal G2 not proved
 496       +--theory PolyPaverExamples: 0/1
 497          +--goal g1 not proved
 498 Replaying tests-provers/polypaver ... OK 2/4 (replay OK)
 499    +--file [../polypaver.why]: 2/4
 500       +--theory TestReal: 2/4
 501          +--goal add1 not proved
 502          +--goal add2 not proved
 503 Replaying tests-provers/strings ... OK 120/128 (replay OK)
 504    +--file [../strings.mlw]: 120/128
 505       +--theory TestString: 56/58
 506          +--goal to_int_lt_0 not proved
 507          +--goal to_int_gt_9 not proved
 508       +--theory TestRegExpr: 41/47
 509          +--goal concat_exists not proved
 510          +--goal in_union not proved
 511          +--goal star1 not proved
 512          +--goal plus_star not proved
 513          +--goal range_not_singleton not proved
 514          +--goal TestPower3 not proved
 515
 516 === Check Builtin translation ===
 517
 518 Replaying check-builtin/ac ... OK 2/2 (replay OK)
 519 Replaying check-builtin/array ... OK 4/4 (replay OK)
 520 Replaying check-builtin/bool ... OK 3/3 (replay OK)
 521 Replaying check-builtin/euclideandivision ... OK 2/2 (replay OK)
 522 Replaying check-builtin/floats ... OK 6/6 (replay OK)
 523 Replaying check-builtin/intreal ... OK 7/7 (replay OK)
 524 Replaying check-builtin/int ... OK 11/11 (replay OK)
 525 Replaying check-builtin/minmax ... OK 2/2 (replay OK)
 526 Replaying check-builtin/propositional ... OK 1/1 (replay OK)
 527 Replaying check-builtin/real ... OK 20/20 (replay OK)
 528
 529 === BTS ===
 530
 531 Replaying bts/114_infix ... OK 0/1 (replay OK)
 532    +--file [../114_infix.mlw]: 0/1
 533       +--theory Test: 0/1
 534          +--goal f not proved
 535 Replaying bts/116_array_access ... OK 0/3 (replay OK)
 536    +--file [../116_array_access.mlw]: 0/3
 537       +--theory Test: 0/3
 538          +--goal a not proved
 539          +--goal f'vc not proved
 540          +--goal c not proved
 541 Replaying bts/12475 ... OK 1/1 (replay OK)
 542 Replaying bts/126_apply ... OK 2/2 (replay OK)
 543 Replaying bts/12934 ... OK 1/1 (replay OK)
 544 Replaying bts/13375 ... OK 0/0 (replay OK)
 545 Replaying bts/13849 ... OK 1/1 (replay OK)
 546 Replaying bts/13853 ... OK 1/1 (replay OK)
 547 Replaying bts/13854 ... OK 2/2 (replay OK)
 548 Replaying bts/138 ... OK 1/1 (replay OK)
 549 Replaying bts/16972 ... OK 1/1 (replay OK)
 550 Replaying bts/16_subst ... OK 0/5 (replay OK)
 551    +--file [../16_subst.mlw]: 0/5
 552       +--theory Issue16: 0/2
 553          +--goal g2 not proved
 554          +--goal g1 not proved
 555       +--theory More: 0/2
 556          +--goal g3 not proved
 557          +--goal g2 not proved
 558       +--theory Other: 0/1
 559          +--goal g not proved
 560 Replaying bts/185_apply_let ... OK 1/1 (replay OK)
 561 Replaying bts/185_apply ... OK 0/3 (replay OK)
 562    +--file [../185_apply.mlw]: 0/3
 563       +--theory Ex1: 0/1
 564          +--goal g not proved
 565       +--theory Ex2: 0/1
 566          +--goal g not proved
 567       +--theory Ex3: 0/1
 568          +--goal g not proved
 569 Replaying bts/19_apply_with ... OK 0/3 (replay OK)
 570    +--file [../19_apply_with.mlw]: 0/3
 571       +--theory I19_simplint: 0/1
 572          +--goal g not proved
 573       +--theory I19_simplpoly: 0/1
 574          +--goal test not proved
 575       +--theory I19_simplpoly2: 0/1
 576          +--goal test not proved
 577 Replaying bts/20445 ... OK 1/2 (replay OK)
 578    +--file [../20445.mlw]: 1/2
 579       +--theory B: 1/2
 580          +--goal G not proved
 581 Replaying bts/231_destruct ... OK 1/7 (replay OK)
 582    +--file [../231_destruct.mlw]: 1/7
 583       +--theory T: 0/1
 584          +--goal G not proved
 585       +--theory T2: 0/1
 586          +--goal G not proved
 587       +--theory Unsoundness: 0/1
 588          +--goal t1 not proved
 589       +--theory Imbrication: 0/1
 590          +--goal G not proved
 591       +--theory Injection: 0/1
 592          +--goal G not proved
 593       +--theory Injection2: 0/1
 594          +--goal G not proved
 595 Replaying bts/244_destruct_rec ... OK 1/1 (replay OK)
 596 Replaying bts/264_destruct_if ... OK 0/9 (replay OK)
 597    +--file [../264_destruct_if.mlw]: 0/9
 598       +--theory Top: 0/9
 599          +--goal g not proved
 600          +--goal g1 not proved
 601          +--goal g2 not proved
 602          +--goal g3 not proved
 603          +--goal g4 not proved
 604          +--goal g5 not proved
 605          +--goal g6 not proved
 606          +--goal g7 not proved
 607          +--goal g8 not proved
 608 Replaying bts/265_apply ... OK 0/4 (replay OK)
 609    +--file [../265_apply.mlw]: 0/4
 610       +--theory Test: 0/1
 611          +--goal g not proved
 612       +--theory Test2: 0/1
 613          +--goal g not proved
 614       +--theory Test3: 0/2
 615          +--goal g1 not proved
 616          +--goal g2 not proved
 617 Replaying bts/269_replace_under_if ... OK 0/1 (replay OK)
 618    +--file [../269_replace_under_if.mlw]: 0/1
 619       +--theory Top: 0/1
 620          +--goal G not proved
 621 Replaying bts/276_shape ... OK 1/1 (replay OK)
 622 Replaying bts/311_destruct ... OK 3/5 (replay OK)
 623    +--file [../311_destruct.mlw]: 3/5
 624       +--theory Top: 3/5
 625          +--goal H2 not proved
 626          +--goal H3 not proved
 627 Replaying bts/380_doc_trans ... OK 3/30 (replay OK)
 628    +--file [../380_doc_trans.mlw]: 3/30
 629       +--theory Apply: 0/1
 630          +--goal G not proved
 631       +--theory Transitivity: 1/2
 632          +--goal transitivity not proved
 633       +--theory Transitivity2: 1/2
 634          +--goal t not proved
 635       +--theory Assert: 0/1
 636          +--goal G not proved
 637       +--theory Case: 0/1
 638          +--goal G not proved
 639       +--theory Destruct: 0/1
 640          +--goal G not proved
 641       +--theory Destruct_rec: 0/1
 642          +--goal G not proved
 643       +--theory Destruct_term: 0/1
 644          +--goal G not proved
 645       +--theory Hide: 0/2
 646          +--goal h not proved
 647          +--goal G not proved
 648       +--theory Induction: 0/1
 649          +--goal G not proved
 650       +--theory Instantiate: 0/1
 651          +--goal G not proved
 652       +--theory Intros: 0/1
 653          +--goal G not proved
 654       +--theory Left: 0/1
 655          +--goal G not proved
 656       +--theory Pose: 0/1
 657          +--goal G not proved
 658       +--theory Remove: 0/2
 659          +--goal h not proved
 660          +--goal G not proved
 661       +--theory Replace: 0/1
 662          +--goal G not proved
 663       +--theory Revert: 0/1
 664          +--goal G not proved
 665       +--theory Rewrite: 0/1
 666          +--goal G not proved
 667       +--theory Rewrite2: 0/1
 668          +--goal G not proved
 669       +--theory Right: 0/1
 670          +--goal G not proved
 671       +--theory Subst: 0/1
 672          +--goal G not proved
 673       +--theory Subst_all: 0/1
 674          +--goal G not proved
 675       +--theory Unfold: 0/2
 676          +--goal h not proved
 677          +--goal G not proved
 678       +--theory Use_th: 0/1
 679          +--goal G not proved
 680 Replaying bts/380_trans_space_args ... OK 0/1 (replay OK)
 681    +--file [../380_trans_space_args.mlw]: 0/1
 682       +--theory Transitivity: 0/1
 683          +--goal G not proved
 684 Replaying bts/450_abs ... OK 8/8 (replay OK)
 685 Replaying bts/548-neg-float-lit ... OK 1/1 (replay OK)
 686 Replaying bts/71_disambiguation ... OK 2/4 (replay OK)
 687    +--file [../71_disambiguation.mlw]: 2/4
 688       +--theory M2: 0/1
 689          +--goal g not proved
 690       +--theory M3: 0/1
 691          +--goal g not proved
 692 Replaying bts/79_compute_unsound ... OK 2/3 (replay OK)
 693    +--file [../79_compute_unsound.mlw]: 2/3
 694       +--theory Soundness: 2/3
 695          +--goal Fail not proved
 696 Replaying bts/destruct_term ... OK 0/1 (replay OK)
 697    +--file [../destruct_term.mlw]: 0/1
 698       +--theory T: 0/1
 699          +--goal f'vc not proved
 700 Replaying bts/fsetint ... OK 0/4 (replay OK)
 701    +--file [../fsetint.why]: 0/4
 702       +--theory Th1: 0/1
 703          +--goal l_false not proved
 704       +--theory Th2: 0/2
 705          +--goal mem_integer not proved
 706          +--goal foo not proved
 707       +--theory Th3: 0/1
 708          +--goal foo not proved
 709
 710 === Logic ===
 711
 712 Replaying logic/agatha ... OK 4/4 (replay OK)
 713 Replaying logic/bitvectors ... FAILED (ret code=1): 20/32 (replay failed)
 714    goal 'g1', prover 'Isabelle 2018': High failure (1.82s),
 715                                       Prover exit status: exited with status 2
 716                                       prover output:
 717                                       *** Unknown Isabelle tool: "why3"
 718
 719                                        instead of Valid (5.26s) (timelimit=0, memlimit=0, steplimit=0)
 720 Replaying logic/bvsum ... OK 3/4 (replay OK)
 721    +--file [../bvsum.mlw]: 3/4
 722       +--theory Mixed: 1/2
 723          +--goal add_bv_int not proved
 724 Replaying logic/distr ... OK 2/2 (replay OK)
 725 Replaying logic/drinker ... OKFile "/users/vals/bbecker/why3/examples/logic/drinker.mlw", line 8, characters 35-57: form "exists x. P -> Q" is likely an error (use "not P \/ Q" if not)
 726  0/1 (replay OK)
 727    +--file [../drinker.mlw]: 0/1
 728       +--theory Top: 0/1
 729          +--goal drinkers_paradox not proved
 730 Replaying logic/einstein ... OK 2/3 (replay OK)
 731    +--file [../einstein.why]: 2/3
 732       +--theory Goals: 2/3
 733          +--goal Wrong not proved
 734 Replaying logic/explicit_subst ... OK 14/14 (replay OK)
 735 Replaying logic/ffx ... OK 7/7 (replay OK)
 736 Replaying logic/First ... OK 2/2 (replay OK)
 737 Replaying logic/genealogy ... FAILED (ret code=1): 7/7 (replay failed)
 738    goal 'Child_is_son_or_daughter', prover 'PVS 6.0': not installed
 739    goal 'Child_is_son_or_daughter', prover 'Isabelle 2018': High failure (1.86s),
 740                                                             Prover exit status: exited with status 2
 741                                                             prover output:
 742                                                             *** Unknown Isabelle tool: "why3"
 743
 744                                                              instead of Valid (6.40s) (timelimit=100, memlimit=4000, steplimit=0)
 745    goal 'Sibling_sym', prover 'Isabelle 2018': High failure (1.82s),
 746                                                Prover exit status: exited with status 2
 747                                                prover output:
 748                                                *** Unknown Isabelle tool: "why3"
 749
 750                                                 instead of Valid (6.03s) (timelimit=100, memlimit=4000, steplimit=0)
 751    goal 'Sibling_is_brother_or_sister', prover 'Isabelle 2018': High failure (1.86s),
 752                                                                 Prover exit status: exited with status 2
 753                                                                 prover output:
 754                                                                 *** Unknown Isabelle tool: "why3"
 755
 756                                                                  instead of Valid (6.26s) (timelimit=100, memlimit=4000, steplimit=0)
 757    goal 'Grandparent_is_grandfather_or_grandmother', prover 'Isabelle 2018':
 758 High failure (1.78s),
 759 Prover exit status: exited with status 2
 760 prover output:
 761 *** Unknown Isabelle tool: "why3"
 762
 763  instead of Valid (6.82s) (timelimit=100, memlimit=4000, steplimit=0)
 764 Replaying logic/hello_proof ... OK 2/3 (replay OK)
 765    +--file [../hello_proof.why]: 2/3
 766       +--theory HelloProof: 2/3
 767          +--goal G2 not proved
 768 Replaying logic/lagrange_inequality ... OK 9/9 (replay OK)
 769 Replaying logic/los_problem ... OK 1/1 (replay OK)
 770 Replaying logic/my_cosine ... FAILED (ret code=1): 4/4 (replay failed)
 771    goal 'MethodError', prover 'Coq 8.9.1': High failure (0.34s),
 772                                            Prover exit status: exited with status 1
 773                                            prover output:
 774                                            File "/tmp/why_b2d3fc_my_cosine_T_MethodError.v", line 17, characters 15-39:
 775 Error:
 776 Cannot find a physical path bound to logical path matching suffix Interval.
 777
 778
 779                                             instead of Valid (1.35s) (timelimit=5, memlimit=1000, steplimit=0)
 780 Replaying logic/real ... FAILED (ret code=1): 1/1 (replay failed)
 781    goal 'MethodError', prover 'Coq 8.9.1': High failure (0.30s),
 782                                            Prover exit status: exited with status 1
 783                                            prover output:
 784                                            File "/tmp/why_d6b037_real_T_MethodError.v", line 15, characters 15-39:
 785 Error:
 786 Cannot find a physical path bound to logical path matching suffix Interval.
 787
 788
 789                                             instead of Valid (1.60s) (timelimit=5, memlimit=1000, steplimit=0)
 790 Replaying logic/scottish-private-club ... OK 1/1 (replay OK)
 791 Replaying logic/simple ... OK 1/1 (replay OK)
 792 Replaying logic/sorted_list ... OK 6/6 (replay OK)
 793 Replaying logic/triangle_inequality ... OK 17/17 (replay OK)
 794 Replaying bitvectors/bitvector ... OK 46/46 (replay OK)
 795 Replaying bitvectors/double_of_int ... OK 63/63 (replay OK)
 796 Replaying bitvectors/double ... OK 7/7 (replay OK)
 797 Replaying bitvectors/neg_as_xor ... OK 13/13 (replay OK)
 798 Replaying bitvectors/power2 ... OK 85/85 (replay OK)
 799
 800 === MLCFG ===
 801
 802 Replaying mlcfg/arith ... OK 2/2 (replay OK)
 803 Replaying mlcfg/basic ... OK 6/6 (replay OK)
 804 Replaying mlcfg/break_continue ... OK 1/1 (replay OK)
 805 Replaying mlcfg/rec ... OK 2/2 (replay OK)
 806 Replaying mlcfg/scope ... OK 0/0 (replay OK)
 807
 808 Summary       : 396/403
 809 Sessions size :  165163 8962133 total
 810 Shapes   size :  10367 2671378 total