ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples/regtests.out

811 lines
37 KiB
Plaintext
Raw Permalink Blame History

=== Programs already ported === MUST REPLAY AND ALL GOALS PROVED ===
Replaying ./add_list_vc_sp ... OK 4/4 (replay OK)
Replaying ./add_list ... OK 4/4 (replay OK)
Replaying ./algo63 ... OK 3/3 (replay OK)
Replaying ./algo64 ... OK 2/2 (replay OK)
Replaying ./algo65 ... OK 1/1 (replay OK)
Replaying ./all_distinct ... OK 1/1 (replay OK)
Replaying ./amortization ... OK 2/2 (replay OK)
Replaying ./arm ... OK 3/3 (replay OK)
Replaying ./array_most_frequent ... OK 1/1 (replay OK)
Replaying ./assigning_meanings_to_programs ... OK 2/2 (replay OK)
Replaying ./bag ... OK 13/13 (replay OK)
Replaying ./balance ... OK 3/3 (replay OK)
Replaying ./bellman_ford ... OK 11/11 (replay OK)
Replaying ./bignum ... OK 5/5 (replay OK)
Replaying ./binary_multiplication ... OK 2/2 (replay OK)
Replaying ./binary_search_vc_sp ... OK 4/4 (replay OK)
Replaying ./binary_search ... OK 9/9 (replay OK)
Replaying ./binary_sort ... OK 2/2 (replay OK)
Replaying ./binary_sqrt ... OK 2/2 (replay OK)
Replaying ./binomial_heap ... OK 23/23 (replay OK)
Replaying ./bitcount ... OK 25/25 (replay OK)
Replaying ./bitvector_examples ... OK 86/86 (replay OK)
Replaying ./bitwalker ... OK 14/14 (replay OK)
Replaying ./braun_trees ... OK 12/12 (replay OK)
Replaying ./bresenham ... OK 2/2 (replay OK)
Replaying ./bubble_sort ... OK 4/4 (replay OK)
Replaying ./checking_a_large_routine ... OK 2/2 (replay OK)
Replaying ./coincidence_count_list ... OK 7/7 (replay OK)
Replaying ./coincidence_count ... OK 9/9 (replay OK)
Replaying ./conjugate ... OK 4/4 (replay OK)
Replaying ./counting_sort ... OK 4/4 (replay OK)
Replaying ./cubic_root ... OK 1/1 (replay OK)
Replaying ./cursor_examples ... OK 26/26 (replay OK)
Replaying ./decrease1 ... OK 3/3 (replay OK)
Replaying ./defunctionalization ... OK 43/43 (replay OK)
Replaying ./dfa_example ... OK 10/10 (replay OK)
Replaying ./dfs ... OK 4/4 (replay OK)
Replaying ./dijkstra ... OK 8/8 (replay OK)
Replaying ./disamb ... OK 10/10 (replay OK)
Replaying ./division ... OK 11/11 (replay OK)
Replaying ./dyck ... OK 4/4 (replay OK)
Replaying ./edit_distance ... OK 13/13 (replay OK)
Replaying ./equality_up_to_spaces ... OK 2/2 (replay OK)
Replaying ./esterel ... OK 5/5 (replay OK)
Replaying ./euler001 ... OK 28/28 (replay OK)
Replaying ./euler002 ... OK 6/6 (replay OK)
Replaying ./euler011 ... OK 5/5 (replay OK)
Replaying ./euler_sieve ... OK 45/45 (replay OK)
Replaying ./ewd673 ... OK 1/1 (replay OK)
Replaying ./fact_vc_sp ... OK 10/10 (replay OK)
Replaying ./fact ... OK 10/10 (replay OK)
Replaying ./fenwick ... OK 5/5 (replay OK)
Replaying ./fib_memo ... OK 2/2 (replay OK)
Replaying ./fibonacci ... OK 27/27 (replay OK)
Replaying ./fill ... OK 1/1 (replay OK)
Replaying ./find ... OK 1/1 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./finger_trees ... OK 3/3 (replay OK)
Replaying ./finite_tarski ... OK 2/2 (replay OK)
Replaying ./flag2 ... OK 12/12 (replay OK)
Replaying ./flag ... OK 1/1 (replay OK)
Replaying ./foveoos11_challenge1 ... OK 1/1 (replay OK)
Replaying ./foveoos11_challenge2 ... OK 2/2 (replay OK)
Replaying ./foveoos11_challenge3 ... OK 1/1 (replay OK)
Replaying ./f_puzzle ... OK 9/9 (replay OK)
Replaying ./gcd_bezout_vc_sp ... OK 1/1 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./gcd_bezout ... OK 1/1 (replay OK)
Replaying ./gcd_vc_sp ... OK 13/13 (replay OK)
Replaying ./gcd ... OK 13/13 (replay OK)
Replaying ./generate_all_trees ... OK 6/6 (replay OK)
Replaying ./gnome_sort ... OK 1/1 (replay OK)
Replaying ./hackers-delight ... OK 51/51 (replay OK)
Replaying ./hashtbl_impl ... OK 11/11 (replay OK)
Replaying ./hillel_challenge ... OK 11/11 (replay OK)
Replaying ./huffman_with_two_queues ... OK 4/4 (replay OK)
Replaying ./induction ... OK 10/10 (replay OK)
Replaying ./infinity_of_primes ... OK 2/2 (replay OK)
Replaying ./insertion_sort_list ... OK 3/3 (replay OK)
Replaying ./insertion_sort_naive ... OK 4/4 (replay OK)
Replaying ./insertion_sort ... OK 6/6 (replay OK)
Replaying ./inverse_in_place ... OK 4/4 (replay OK)
Replaying ./isqrt_von_neumann ... OK 6/6 (replay OK)
Replaying ./isqrt ... OK 6/6 (replay OK)
Replaying ./kleene_algebra ... OK 83/83 (replay OK)
Replaying ./kmp ... OK 13/13 (replay OK)
Replaying ./knuth_prime_numbers ... OK 3/3 (replay OK)
Replaying ./koda_ruskey ... OK 40/40 (replay OK)
Replaying ./largest_prime_factor ... OK 4/4 (replay OK)
Replaying ./lcp ... OK 2/2 (replay OK)
Replaying ./leftist_heap ... OK 13/13 (replay OK)
Replaying ./linear_probing ... OK 16/16 (replay OK)
Replaying ./linked_list_rev ... OK 22/22 (replay OK)
Replaying ./list_removal ... OK 8/8 (replay OK)
Replaying ./maximum_subarray ... OK 7/7 (replay OK)
Replaying ./max_matrix ... OK 4/4 (replay OK)
Replaying ./mccarthy_vc_sp ... OK 6/6 (replay OK)
Replaying ./mccarthy ... OK 11/11 (replay OK)
Replaying ./mergesort_array ... OK 9/9 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./mergesort_list ... OK 20/20 (replay OK)
Replaying ./mergesort_queue ... OK 5/5 (replay OK)
Replaying ./mex ... OK 2/2 (replay OK)
Replaying ./min_max ... OK 4/4 (replay OK)
Replaying ./mjrty ... OK 1/1 (replay OK)
Replaying ./muller ... OK 1/1 (replay OK)
Replaying ./mutual_recursion ... OK 4/4 (replay OK)
Replaying ./my_cosine ... FAILED (ret code=1): 1/1 (replay failed)
goal 'my_cosine'vc.0', prover 'Coq 8.9.1': High failure (0.29s),
Prover exit status: exited with status 1
prover output:
File "/tmp/why_48a7c6_my_cosine_T_my_cosineqtvc.v", line 136, characters 15-39:
Error:
Cannot find a physical path bound to logical path matching suffix Interval.
instead of Valid (1.61s) (timelimit=5, memlimit=1000, steplimit=0)
Replaying ./nistonacci ... OK 4/4 (replay OK)
Replaying ./optimal_replay ... OK 1/1 (replay OK)
Replaying ./pairing_heap_bin ... OK 16/16 (replay OK)
Replaying ./pairing_heap ... OK 31/31 (replay OK)
Replaying ./pancake_sorting ... OK 2/2 (replay OK)
Replaying ./patience ... OK 8/8 (replay OK)
Replaying ./pigeonhole ... OK 2/2 (replay OK)
Replaying ./power_vc_sp ... OK 2/2 (replay OK)
Replaying ./power ... OK 2/2 (replay OK)
Replaying ./queens_bv ... OK 16/16 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./queens ... OK 5/5 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./queue_two_lists ... OK 25/25 (replay OK)
Replaying ./quicksort ... OK 12/12 (replay OK)
Replaying ./random_access_list ... OK 20/20 (replay OK)
Replaying ./register_allocation ... OK 12/12 (replay OK)
Replaying ./relabel ... OK 4/4 (replay OK)
Replaying ./remove_duplicate_hash ... OK 1/1 (replay OK)
Replaying ./remove_duplicate ... OK 2/2 (replay OK)
Replaying ./residual ... OK 5/5 (replay OK)
Replaying ./resizable_array ... OK 8/8 (replay OK)
Replaying ./rightmostbittrick ... OK 2/2 (replay OK)
Replaying ./ring_buffer ... OK 4/4 (replay OK)
Replaying ./ropes ... OK 17/17 (replay OK)
Replaying ./same_fringe ... OK 3/3 (replay OK)
Replaying ./schorr_waite_via_recursion ... OK 2/2 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./schorr_waite ... OK 7/7 (replay OK)
Replaying ./schorr_waite_with_ghost_monitor ... OK 1/1 (replay OK)
Replaying ./selection_sort ... OK 4/4 (replay OK)
Replaying ./sf ... OK 10/10 (replay OK)
Replaying ./sieve ... OK 2/2 (replay OK)
Replaying ./skew_heaps ... OK 7/7 (replay OK)
Replaying ./snapshotable_trees ... OK 13/13 (replay OK)
Replaying ./sorted_list ... OK 2/2 (replay OK)
Replaying ./string_base64_encoding ... OK 14/14 (replay OK)
Replaying ./string_hex_encoding ... OK 6/6 (replay OK)
Replaying ./string_search ... OK 8/8 (replay OK)
Replaying ./subsequence ... OK 1/1 (replay OK)
Replaying ./sudoku ... OK 20/20 (replay OK)
Replaying ./sumrange ... OK 20/20 (replay OK)
Replaying ./swap ... OK 4/4 (replay OK)
Replaying ./there_and_back_again ... OK 4/4 (replay OK)
Replaying ./three_idem_ring ... OK 27/27 (replay OK)
Replaying ./topological_sorting ... OK 5/5 (replay OK)
Replaying ./tortoise_and_hare ... OK 4/4 (replay OK)
Replaying ./tower_of_hanoi ... OK 9/9 (replay OK)
Replaying ./toy_compiler ... OK 2/2 (replay OK)
Replaying ./tree_height ... OK 11/11 (replay OK)
Replaying ./tree_of_array ... OK 2/2 (replay OK)
Replaying ./tree_of_list ... OK 2/2 (replay OK)
Replaying ./unraveling_a_card_trick ... OK 5/5 (replay OK)
Replaying ./vacid_0_build_maze ... OK 3/3 (replay OK)
Replaying ./vacid_0_red_black_trees ... OK 37/37 (replay OK)
Replaying ./vacid_0_sparse_array ... OK 8/8 (replay OK)
Replaying ./verifythis_2015_dancing_links ... OK 3/3 (replay OK)
Replaying ./verifythis_2015_parallel_gcd ... OK 6/6 (replay OK)
Replaying ./verifythis_2015_relaxed_prefix ... OK 1/1 (replay OK)
Replaying ./verifythis_2016_tree_traversal ... OK 10/10 (replay OK)
Replaying ./verifythis_2017_maximum_sum_submatrix ... OK 1/1 (replay OK)
Replaying ./verifythis_2017_odd_even_sort_rearranging ... OK 8/8 (replay OK)
Replaying ./verifythis_2017_odd_even_transposition_sort ... OK 2/2 (replay OK)
Replaying ./verifythis_2017_pair_insertion_sort ... OK 1/1 (replay OK)
Replaying ./verifythis_2017_tree_buffer ... OK 10/10 (replay OK)
Replaying ./verifythis_2018_array_based_queuing_lock_1 ... OK 8/8 (replay OK)
Replaying ./verifythis_2018_array_based_queuing_lock_2 ... OK 10/10 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./verifythis_2018_le_rouge_et_le_noir_1 ... OK 23/23 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./verifythis_2018_le_rouge_et_le_noir_2 ... OK 8/8 (replay OK)
Replaying ./verifythis_2018_mind_the_gap_1 ... OK 6/6 (replay OK)
Replaying ./verifythis_2018_mind_the_gap_2 ... OK 6/6 (replay OK)
Replaying ./verifythis_2018_register_allocation ... OK 10/10 (replay OK)
Replaying ./verifythis_2019_cartesian_trees ... OK 15/15 (replay OK)
Replaying ./verifythis_2019_ghc_sort ... OK 24/24 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./verifythis_2021_dll_to_bst ... OKSymbol '([])'result'unused'unused' not found, ignored
Symbol '(=)'result'unused'unused' not found, ignored
Symbol '([])'result'unused'unused' not found, ignored
Symbol '(=)'result'unused'unused' not found, ignored
Symbol '([])'result'unused'unused' not found, ignored
Symbol '(=)'result'unused'unused' not found, ignored
Symbol '([])'result'unused'unused' not found, ignored
Symbol '(=)'result'unused'unused' not found, ignored
Symbol '([])'result'unused'unused' not found, ignored
Symbol '(=)'result'unused'unused' not found, ignored
Symbol '([])'result'unused'unused' not found, ignored
Symbol '(=)'result'unused'unused' not found, ignored
10/10 (replay OK)
Replaying ./verifythis_2021_lexicographic_permutations_1 ... OK 17/17 (replay OK)
Replaying ./verifythis_2021_lexicographic_permutations_2 ... OK 27/27 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying ./verifythis_2021_shearsort_modified ... OK 2/2 (replay OK)
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
12/12 (replay OK)
Replaying ./verifythis_fm2012_LRS ... OK 20/20 (replay OK)
Replaying ./verifythis_fm2012_treedel ... OK 12/12 (replay OK)
Replaying ./verifythis_PrefixSumRec ... OK 9/9 (replay OK)
Replaying ./vstte10_aqueue ... OK 6/6 (replay OK)
Replaying ./vstte10_inverting ... OK 3/3 (replay OK)
Replaying ./vstte10_max_sum ... OK 3/3 (replay OK)
Replaying ./vstte10_queens ... OK 17/17 (replay OK)
Replaying ./vstte10_search_list ... OK 5/5 (replay OK)
Replaying ./vstte12_bfs ... OK 6/6 (replay OK)
Replaying ./vstte12_combinators ... OK 12/12 (replay OK)
Replaying ./vstte12_ring_buffer ... OK 20/20 (replay OK)
Replaying ./vstte12_tree_reconstruction ... OK 23/23 (replay OK)
Replaying ./vstte12_two_way_sort ... OK 1/1 (replay OK)
Replaying ./warshall_algorithm ... OK 3/3 (replay OK)
Replaying ./white_and_black_balls ... OK 1/1 (replay OK)
Replaying ./word_common_factor ... OK 3/3 (replay OK)
Replaying ./wrap_lines ... OK 6/6 (replay OK)
Replaying ./zeros ... OK 7/7 (replay OK)
Replaying micro-c/dicho ... OK 2/2 (replay OK)
Replaying micro-c/isqrt ... OK 1/1 (replay OK)
Replaying micro-c/loops ... OK 2/2 (replay OK)
Replaying micro-c/mult ... OK 1/1 (replay OK)
Replaying micro-c/sort ... OK 2/2 (replay OK)
Replaying micro-c/triangular ... OK 3/3 (replay OK)
Replaying python/arrays ... OK 1/1 (replay OK)
Replaying python/break_continue ... OK 1/1 (replay OK)
Replaying python/check_duplicates ... OK 1/1 (replay OK)
Replaying python/concat ... OK 1/1 (replay OK)
Replaying python/dicho ... OK 1/1 (replay OK)
Replaying python/even ... OK 1/1 (replay OK)
Replaying python/fact ... OK 1/1 (replay OK)
Replaying python/isqrt_fun ... OK 1/1 (replay OK)
Replaying python/isqrt ... OK 1/1 (replay OK)
Replaying python/is_sorted ... OK 1/1 (replay OK)
Replaying python/mult ... OK 1/1 (replay OK)
Replaying python/nim ... OK 1/1 (replay OK)
Replaying python/pgcd ... OK 1/1 (replay OK)
Replaying python/range ... OK 1/1 (replay OK)
Replaying python/reverse ... OK 1/1 (replay OK)
Replaying python/sort ... OK 1/1 (replay OK)
Replaying python/sum_reverse ... OK 1/1 (replay OK)
Replaying python/triangular ... OK 1/1 (replay OK)
Replaying double_wp/compiler ... OK 9/9 (replay OK)
Replaying double_wp/imp ... OK 2/2 (replay OK)
Replaying double_wp/logic ... OK 12/12 (replay OK)
Replaying double_wp/specs ... OK 15/15 (replay OK)
Replaying double_wp/state ... OK 0/0 (replay OK)
Replaying double_wp/vm ... OK 4/4 (replay OK)
Replaying avl/avl ... OK 31/31 (replay OK)
Replaying avl/key_type ... OK 0/0 (replay OK)
Replaying avl/monoid ... OK 8/8 (replay OK)
Replaying avl/preorder ... OK 7/7 (replay OK)
Replaying avl/priority_queue ... OK 34/34 (replay OK)
Replaying avl/ral ... OK 37/37 (replay OK)
Replaying avl/tables ... OK 106/106 (replay OK)
Replaying c_cursor/ccursor ... OK 5/5 (replay OK)
Replaying foveoos11-cm/array_max ... OK 1/1 (replay OK)
Replaying foveoos11-cm/duplets ... OK 2/2 (replay OK)
Replaying foveoos11-cm/tree_max ... OK 3/3 (replay OK)
Replaying vacid_0_binary_heaps/proofs ... OK 38/38 (replay OK)
Replaying verifythis_2016_matrix_multiplication/matrices_ring_simp ... OK 23/23 (replay OK)
Replaying verifythis_2016_matrix_multiplication/matrices ... OK 23/23 (replay OK)
Replaying verifythis_2016_matrix_multiplication/naive ... OK 1/1 (replay OK)
Replaying verifythis_2016_matrix_multiplication/strassen ... OK 14/14 (replay OK)
Replaying verifythis_2016_matrix_multiplication/sum_extended ... OK 4/4 (replay OK)
Replaying WP_revisited/blocking_semantics5 ... OK 38/38 (replay OK)
Replaying WP_revisited/formula ... OK 1/1 (replay OK)
Replaying WP_revisited/imp_n ... OK 18/18 (replay OK)
Replaying WP_revisited/wp2 ... OK 30/30 (replay OK)
Replaying prover/BacktrackArray ... OK 8/8 (replay OK)
Replaying prover/Choice ... OK 0/0 (replay OK)
Replaying prover/Firstorder_formula_impl ... OK 16/16 (replay OK)
Replaying prover/Firstorder_formula_list_impl ... OK 16/16 (replay OK)
Replaying prover/Firstorder_formula_list_spec ... OK 25/25 (replay OK)
Replaying prover/Firstorder_formula_spec ... OK 25/25 (replay OK)
Replaying prover/Firstorder_semantics ... OK 24/24 (replay OK)
Replaying prover/Firstorder_symbol_impl ... OK 12/12 (replay OK)
Replaying prover/Firstorder_symbol_spec ... OK 32/32 (replay OK)
Replaying prover/Firstorder_tableau_impl ... OK 16/16 (replay OK)
Replaying prover/Firstorder_tableau_spec ... OK 25/25 (replay OK)
Replaying prover/Firstorder_term_impl ... OK 33/33 (replay OK)
Replaying prover/Firstorder_term_spec ... OK 64/64 (replay OK)
Replaying prover/FormulaTransformations ... OK 27/27 (replay OK)
Replaying prover/Functions ... OK 6/6 (replay OK)
Replaying prover/ISet ... OK 4/4 (replay OK)
Replaying prover/Nat ... OK 3/3 (replay OK)
Replaying prover/OptionFuncs ... OK 12/12 (replay OK)
Replaying prover/Predicates ... OK 4/4 (replay OK)
Replaying prover/ProverMain ... OK 1/1 (replay OK)
Replaying prover/ProverTest ... OK 14/14 (replay OK)
Replaying prover/Prover ... OK 16/16 (replay OK)
Replaying prover/Sum ... OK 0/0 (replay OK)
Replaying prover/Unification ... OK 11/11 (replay OK)
Replaying multiprecision/add_1 ... OK 4/4 (replay OK)
Replaying multiprecision/add ... OK 12/12 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/base_info ... OK 5/5 (replay OK)
Replaying multiprecision/compare ... OK 1/1 (replay OK)
Replaying multiprecision/div ... OK 13/13 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/get_str ... OK 4/4 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/lemmas ... OK 25/25 (replay OK)
Replaying multiprecision/lineardecision ... OK 226/226 (replay OK)
Replaying multiprecision/logical ... OK 13/13 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/mpz_abs ... OK 1/1 (replay OK)
Replaying multiprecision/mpz_add ... OK 2/2 (replay OK)
Replaying multiprecision/mpz_cmpabs ... OK 3/3 (replay OK)
Replaying multiprecision/mpz_cmp ... OK 4/4 (replay OK)
Replaying multiprecision/mpz_div2exp ... OK 3/3 (replay OK)
Replaying multiprecision/mpz_div ... OK 2/2 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/mpz_getset ... OK 4/4 (replay OK)
Replaying multiprecision/mpz_get_str ... OK 3/3 (replay OK)
Replaying multiprecision/mpz_mul2exp ... OK 1/1 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/mpz_mul ... OK 3/3 (replay OK)
Replaying multiprecision/mpz_neg ... OK 1/1 (replay OK)
Replaying multiprecision/mpz_realloc2 ... OK 1/1 (replay OK)
Replaying multiprecision/mpz_set_str ... OK 1/1 (replay OK)
Replaying multiprecision/mpz_sub ... OK 3/3 (replay OK)
Replaying multiprecision/mpz ... OK 9/9 (replay OK)
Replaying multiprecision/mul ... OK 7/7 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/powm ... OK 18/18 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/set_str ... OK 3/3 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/sqrtrem ... OK 6/6 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/sqrt ... OK 3/3 (replay OK)
Replaying multiprecision/stringlemmas ... OK 40/40 (replay OK)
Replaying multiprecision/sub_1 ... OK 4/4 (replay OK)
Replaying multiprecision/sub ... OK 12/12 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/toom ... OK 8/8 (replay OK, obsolete session)
[Warning] session is obsolete
Replaying multiprecision/types ... OK 0/0 (replay OK)
Replaying multiprecision/util ... OK 7/7 (replay OK)
Replaying multiprecision/valuation ... OK 14/14 (replay OK)
Replaying multiprecision/wmpn ... OK 0/0 (replay OK)
Score on ported programs : 310/311
=== Standard Library ===
Replaying stdlib/array ... OK 22/22 (replay OK)
Replaying stdlib/bintree ... OK 6/6 (replay OK)
Replaying stdlib/byte_string ... OK 2/2 (replay OK)
Replaying stdlib/list ... OK 54/54 (replay OK)
Replaying stdlib/pigeon ... OK 4/6 (replay OK)
+--file [../../../stdlib/pigeon.mlw]: 4/6
+--theory ListAndSet: 3/5
+--goal corner not proved
+--goal pigeon_1 not proved
Replaying stdlib/pqueue ... OK 5/5 (replay OK)
Replaying stdlib/stringCheck ... OK 60/60 (replay OK)
Replaying stdlib/tagset ... OK 14/14 (replay OK)
Replaying stdlib/witness ... OK 1/1 (replay OK)
=== Tests ===
Replaying tests-provers/bitvec ... OK 6/6 (replay OK)
Replaying tests-provers/bv ... OK 157/198 (replay OK)
+--file [../bv.why]: 157/198
+--theory CheckBV64: 58/71
+--goal trap not proved
+--goal smoke1 not proved
+--goal smoke2 not proved
+--goal smoke3 not proved
+--goal smoke4 not proved
+--goal smoke5 not proved
+--goal smoke6 not proved
+--goal smoke7 not proved
+--goal smoke8 not proved
+--goal f1 not proved
+--goal f2 not proved
+--goal f3 not proved
+--goal f7 not proved
+--theory CheckBV32: 33/42
+--goal trap not proved
+--goal smoke1 not proved
+--goal smoke2 not proved
+--goal smoke3 not proved
+--goal smoke4 not proved
+--goal smoke5 not proved
+--goal smoke6 not proved
+--goal smoke7 not proved
+--goal smoke8 not proved
+--theory CheckBV16: 33/42
+--goal trap not proved
+--goal smoke1 not proved
+--goal smoke2 not proved
+--goal smoke3 not proved
+--goal smoke4 not proved
+--goal smoke5 not proved
+--goal smoke6 not proved
+--goal smoke7 not proved
+--goal smoke8 not proved
+--theory CheckBV8: 33/42
+--goal trap not proved
+--goal smoke1 not proved
+--goal smoke2 not proved
+--goal smoke3 not proved
+--goal smoke4 not proved
+--goal smoke5 not proved
+--goal smoke6 not proved
+--goal smoke7 not proved
+--goal smoke8 not proved
+--theory Extras: 0/1
+--goal mod_mult not proved
Replaying tests-provers/ceil ... OK 12/12 (replay OK)
Replaying tests-provers/coq-interval ... FAILED (ret code=1): 0/1 (replay failed)
goal 'pow_eps2_max_int', prover 'Coq 8.9.1': High failure (0.28s),
Prover exit status: exited with status 1
prover output:
File "/tmp/why_f8d102_coqmninterval_T_pow_eps2_max_int.v", line 11, characters 15-39:
Error:
Cannot find a physical path bound to logical path matching suffix Interval.
instead of Valid (0.77s) (timelimit=5, memlimit=1000, steplimit=0)
Replaying tests-provers/coq ... OK 1/1 (replay OK)
Replaying tests-provers/cvc3 ... OK 1/3 (replay OK)
+--file [../cvc3.why]: 1/3
+--theory Test: 1/3
+--goal test1 not proved
+--goal test2 not proved
Replaying tests-provers/div_real ... OK 9/12 (replay OK)
+--file [../div_real.why]: 9/12
+--theory DivTest: 9/12
+--goal smoke1 not proved
+--goal smoke3 not proved
+--goal smoke5 not proved
Replaying tests-provers/div ... OK 13/25 (replay OK)
+--file [../div.why]: 13/25
+--theory EuclideanDivTest: 6/12
+--goal smoke1 not proved
+--goal smoke2 not proved
+--goal smoke3 not proved
+--goal smoke4 not proved
+--goal smoke5 not proved
+--goal smoke6 not proved
+--theory ComputerDivTest: 7/13
+--goal smoke1 not proved
+--goal smoke2 not proved
+--goal smoke3 not proved
+--goal smoke4 not proved
+--goal smoke5 not proved
+--goal smoke6 not proved
Replaying tests-provers/gappa ... OK 14/14 (replay OK)
Replaying tests-provers/ieee_float ... FAILED (ret code=1): 16/20 (replay failed)
goal 'wrong', prover 'Isabelle 2018': High failure (1.82s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Unknown () (7.18s) (timelimit=0, memlimit=0, steplimit=0)
goal 'ok', prover 'Isabelle 2018': High failure (1.87s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (6.95s) (timelimit=0, memlimit=0, steplimit=0)
goal 'more', prover 'Isabelle 2018': High failure (1.84s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (7.22s) (timelimit=0, memlimit=0, steplimit=0)
Replaying tests-provers/metitarski ... OK 5/11 (replay OK)
+--file [../metitarski.why]: 5/11
+--theory P3: 2/4
+--goal cos_bound not proved
+--goal MethodErrorWrong not proved
+--theory Power: 0/3
+--goal G not proved
+--goal G1 not proved
+--goal G2 not proved
+--theory PolyPaverExamples: 0/1
+--goal g1 not proved
Replaying tests-provers/polypaver ... OK 2/4 (replay OK)
+--file [../polypaver.why]: 2/4
+--theory TestReal: 2/4
+--goal add1 not proved
+--goal add2 not proved
Replaying tests-provers/strings ... OK 120/128 (replay OK)
+--file [../strings.mlw]: 120/128
+--theory TestString: 56/58
+--goal to_int_lt_0 not proved
+--goal to_int_gt_9 not proved
+--theory TestRegExpr: 41/47
+--goal concat_exists not proved
+--goal in_union not proved
+--goal star1 not proved
+--goal plus_star not proved
+--goal range_not_singleton not proved
+--goal TestPower3 not proved
=== Check Builtin translation ===
Replaying check-builtin/ac ... OK 2/2 (replay OK)
Replaying check-builtin/array ... OK 4/4 (replay OK)
Replaying check-builtin/bool ... OK 3/3 (replay OK)
Replaying check-builtin/euclideandivision ... OK 2/2 (replay OK)
Replaying check-builtin/floats ... OK 6/6 (replay OK)
Replaying check-builtin/intreal ... OK 7/7 (replay OK)
Replaying check-builtin/int ... OK 11/11 (replay OK)
Replaying check-builtin/minmax ... OK 2/2 (replay OK)
Replaying check-builtin/propositional ... OK 1/1 (replay OK)
Replaying check-builtin/real ... OK 20/20 (replay OK)
=== BTS ===
Replaying bts/114_infix ... OK 0/1 (replay OK)
+--file [../114_infix.mlw]: 0/1
+--theory Test: 0/1
+--goal f not proved
Replaying bts/116_array_access ... OK 0/3 (replay OK)
+--file [../116_array_access.mlw]: 0/3
+--theory Test: 0/3
+--goal a not proved
+--goal f'vc not proved
+--goal c not proved
Replaying bts/12475 ... OK 1/1 (replay OK)
Replaying bts/126_apply ... OK 2/2 (replay OK)
Replaying bts/12934 ... OK 1/1 (replay OK)
Replaying bts/13375 ... OK 0/0 (replay OK)
Replaying bts/13849 ... OK 1/1 (replay OK)
Replaying bts/13853 ... OK 1/1 (replay OK)
Replaying bts/13854 ... OK 2/2 (replay OK)
Replaying bts/138 ... OK 1/1 (replay OK)
Replaying bts/16972 ... OK 1/1 (replay OK)
Replaying bts/16_subst ... OK 0/5 (replay OK)
+--file [../16_subst.mlw]: 0/5
+--theory Issue16: 0/2
+--goal g2 not proved
+--goal g1 not proved
+--theory More: 0/2
+--goal g3 not proved
+--goal g2 not proved
+--theory Other: 0/1
+--goal g not proved
Replaying bts/185_apply_let ... OK 1/1 (replay OK)
Replaying bts/185_apply ... OK 0/3 (replay OK)
+--file [../185_apply.mlw]: 0/3
+--theory Ex1: 0/1
+--goal g not proved
+--theory Ex2: 0/1
+--goal g not proved
+--theory Ex3: 0/1
+--goal g not proved
Replaying bts/19_apply_with ... OK 0/3 (replay OK)
+--file [../19_apply_with.mlw]: 0/3
+--theory I19_simplint: 0/1
+--goal g not proved
+--theory I19_simplpoly: 0/1
+--goal test not proved
+--theory I19_simplpoly2: 0/1
+--goal test not proved
Replaying bts/20445 ... OK 1/2 (replay OK)
+--file [../20445.mlw]: 1/2
+--theory B: 1/2
+--goal G not proved
Replaying bts/231_destruct ... OK 1/7 (replay OK)
+--file [../231_destruct.mlw]: 1/7
+--theory T: 0/1
+--goal G not proved
+--theory T2: 0/1
+--goal G not proved
+--theory Unsoundness: 0/1
+--goal t1 not proved
+--theory Imbrication: 0/1
+--goal G not proved
+--theory Injection: 0/1
+--goal G not proved
+--theory Injection2: 0/1
+--goal G not proved
Replaying bts/244_destruct_rec ... OK 1/1 (replay OK)
Replaying bts/264_destruct_if ... OK 0/9 (replay OK)
+--file [../264_destruct_if.mlw]: 0/9
+--theory Top: 0/9
+--goal g not proved
+--goal g1 not proved
+--goal g2 not proved
+--goal g3 not proved
+--goal g4 not proved
+--goal g5 not proved
+--goal g6 not proved
+--goal g7 not proved
+--goal g8 not proved
Replaying bts/265_apply ... OK 0/4 (replay OK)
+--file [../265_apply.mlw]: 0/4
+--theory Test: 0/1
+--goal g not proved
+--theory Test2: 0/1
+--goal g not proved
+--theory Test3: 0/2
+--goal g1 not proved
+--goal g2 not proved
Replaying bts/269_replace_under_if ... OK 0/1 (replay OK)
+--file [../269_replace_under_if.mlw]: 0/1
+--theory Top: 0/1
+--goal G not proved
Replaying bts/276_shape ... OK 1/1 (replay OK)
Replaying bts/311_destruct ... OK 3/5 (replay OK)
+--file [../311_destruct.mlw]: 3/5
+--theory Top: 3/5
+--goal H2 not proved
+--goal H3 not proved
Replaying bts/380_doc_trans ... OK 3/30 (replay OK)
+--file [../380_doc_trans.mlw]: 3/30
+--theory Apply: 0/1
+--goal G not proved
+--theory Transitivity: 1/2
+--goal transitivity not proved
+--theory Transitivity2: 1/2
+--goal t not proved
+--theory Assert: 0/1
+--goal G not proved
+--theory Case: 0/1
+--goal G not proved
+--theory Destruct: 0/1
+--goal G not proved
+--theory Destruct_rec: 0/1
+--goal G not proved
+--theory Destruct_term: 0/1
+--goal G not proved
+--theory Hide: 0/2
+--goal h not proved
+--goal G not proved
+--theory Induction: 0/1
+--goal G not proved
+--theory Instantiate: 0/1
+--goal G not proved
+--theory Intros: 0/1
+--goal G not proved
+--theory Left: 0/1
+--goal G not proved
+--theory Pose: 0/1
+--goal G not proved
+--theory Remove: 0/2
+--goal h not proved
+--goal G not proved
+--theory Replace: 0/1
+--goal G not proved
+--theory Revert: 0/1
+--goal G not proved
+--theory Rewrite: 0/1
+--goal G not proved
+--theory Rewrite2: 0/1
+--goal G not proved
+--theory Right: 0/1
+--goal G not proved
+--theory Subst: 0/1
+--goal G not proved
+--theory Subst_all: 0/1
+--goal G not proved
+--theory Unfold: 0/2
+--goal h not proved
+--goal G not proved
+--theory Use_th: 0/1
+--goal G not proved
Replaying bts/380_trans_space_args ... OK 0/1 (replay OK)
+--file [../380_trans_space_args.mlw]: 0/1
+--theory Transitivity: 0/1
+--goal G not proved
Replaying bts/450_abs ... OK 8/8 (replay OK)
Replaying bts/548-neg-float-lit ... OK 1/1 (replay OK)
Replaying bts/71_disambiguation ... OK 2/4 (replay OK)
+--file [../71_disambiguation.mlw]: 2/4
+--theory M2: 0/1
+--goal g not proved
+--theory M3: 0/1
+--goal g not proved
Replaying bts/79_compute_unsound ... OK 2/3 (replay OK)
+--file [../79_compute_unsound.mlw]: 2/3
+--theory Soundness: 2/3
+--goal Fail not proved
Replaying bts/destruct_term ... OK 0/1 (replay OK)
+--file [../destruct_term.mlw]: 0/1
+--theory T: 0/1
+--goal f'vc not proved
Replaying bts/fsetint ... OK 0/4 (replay OK)
+--file [../fsetint.why]: 0/4
+--theory Th1: 0/1
+--goal l_false not proved
+--theory Th2: 0/2
+--goal mem_integer not proved
+--goal foo not proved
+--theory Th3: 0/1
+--goal foo not proved
=== Logic ===
Replaying logic/agatha ... OK 4/4 (replay OK)
Replaying logic/bitvectors ... FAILED (ret code=1): 20/32 (replay failed)
goal 'g1', prover 'Isabelle 2018': High failure (1.82s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (5.26s) (timelimit=0, memlimit=0, steplimit=0)
Replaying logic/bvsum ... OK 3/4 (replay OK)
+--file [../bvsum.mlw]: 3/4
+--theory Mixed: 1/2
+--goal add_bv_int not proved
Replaying logic/distr ... OK 2/2 (replay OK)
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)
0/1 (replay OK)
+--file [../drinker.mlw]: 0/1
+--theory Top: 0/1
+--goal drinkers_paradox not proved
Replaying logic/einstein ... OK 2/3 (replay OK)
+--file [../einstein.why]: 2/3
+--theory Goals: 2/3
+--goal Wrong not proved
Replaying logic/explicit_subst ... OK 14/14 (replay OK)
Replaying logic/ffx ... OK 7/7 (replay OK)
Replaying logic/First ... OK 2/2 (replay OK)
Replaying logic/genealogy ... FAILED (ret code=1): 7/7 (replay failed)
goal 'Child_is_son_or_daughter', prover 'PVS 6.0': not installed
goal 'Child_is_son_or_daughter', prover 'Isabelle 2018': High failure (1.86s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (6.40s) (timelimit=100, memlimit=4000, steplimit=0)
goal 'Sibling_sym', prover 'Isabelle 2018': High failure (1.82s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (6.03s) (timelimit=100, memlimit=4000, steplimit=0)
goal 'Sibling_is_brother_or_sister', prover 'Isabelle 2018': High failure (1.86s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (6.26s) (timelimit=100, memlimit=4000, steplimit=0)
goal 'Grandparent_is_grandfather_or_grandmother', prover 'Isabelle 2018':
High failure (1.78s),
Prover exit status: exited with status 2
prover output:
*** Unknown Isabelle tool: "why3"
instead of Valid (6.82s) (timelimit=100, memlimit=4000, steplimit=0)
Replaying logic/hello_proof ... OK 2/3 (replay OK)
+--file [../hello_proof.why]: 2/3
+--theory HelloProof: 2/3
+--goal G2 not proved
Replaying logic/lagrange_inequality ... OK 9/9 (replay OK)
Replaying logic/los_problem ... OK 1/1 (replay OK)
Replaying logic/my_cosine ... FAILED (ret code=1): 4/4 (replay failed)
goal 'MethodError', prover 'Coq 8.9.1': High failure (0.34s),
Prover exit status: exited with status 1
prover output:
File "/tmp/why_b2d3fc_my_cosine_T_MethodError.v", line 17, characters 15-39:
Error:
Cannot find a physical path bound to logical path matching suffix Interval.
instead of Valid (1.35s) (timelimit=5, memlimit=1000, steplimit=0)
Replaying logic/real ... FAILED (ret code=1): 1/1 (replay failed)
goal 'MethodError', prover 'Coq 8.9.1': High failure (0.30s),
Prover exit status: exited with status 1
prover output:
File "/tmp/why_d6b037_real_T_MethodError.v", line 15, characters 15-39:
Error:
Cannot find a physical path bound to logical path matching suffix Interval.
instead of Valid (1.60s) (timelimit=5, memlimit=1000, steplimit=0)
Replaying logic/scottish-private-club ... OK 1/1 (replay OK)
Replaying logic/simple ... OK 1/1 (replay OK)
Replaying logic/sorted_list ... OK 6/6 (replay OK)
Replaying logic/triangle_inequality ... OK 17/17 (replay OK)
Replaying bitvectors/bitvector ... OK 46/46 (replay OK)
Replaying bitvectors/double_of_int ... OK 63/63 (replay OK)
Replaying bitvectors/double ... OK 7/7 (replay OK)
Replaying bitvectors/neg_as_xor ... OK 13/13 (replay OK)
Replaying bitvectors/power2 ... OK 85/85 (replay OK)
=== MLCFG ===
Replaying mlcfg/arith ... OK 2/2 (replay OK)
Replaying mlcfg/basic ... OK 6/6 (replay OK)
Replaying mlcfg/break_continue ... OK 1/1 (replay OK)
Replaying mlcfg/rec ... OK 2/2 (replay OK)
Replaying mlcfg/scope ... OK 0/0 (replay OK)
Summary : 396/403
Sessions size : 165163 8962133 total
Shapes size : 10367 2671378 total
Reference in New Issue View Git Blame Copy Permalink