Resolve "Internal error in Alt-ergo after inline_trivial"
Closes #417
Merge request reports
Activity
added To be discussed label
requested review from @marche
assigned to @pbonnot
added 1 commit
- f170b391 - Changed alt-ergo drivers so that we don't unfold basic arithmetic symbols
mentioned in merge request !875 (merged)
removed To be discussed label
added ProofInUse/TrustInSoft label
added 51 commits
-
b9ed009b...999af568 - 49 commits from branch
master
- 284b5dd5 - Merge branch 'master' into 417-internal-error-in-alt-ergo-after-inline_trivial
- bce98d11 - fix coq proof for coq old versions
-
b9ed009b...999af568 - 49 commits from branch
added 1 commit
- 16e4367c - diff in bench-api directly copied into oracle
Not only the update of Coq proofs do not work on old coq version, but there are quite a lot of failed examples. The change does not worth the effort
Replaying ./coincidence_count ... FAILED (ret code=1): 8/9 (replay failed) Replaying ./euler001 ... FAILED (ret code=1): 28/29 (replay failed) Replaying ./euler002 ... FAILED (ret code=1): 6/7 (replay failed) Replaying ./euler_sieve ... FAILED (ret code=1): 43/45 (replay failed) Replaying ./foveoos11_challenge2 ... FAILED (ret code=1): 1/2 (replay failed) Replaying ./gcd_vc_sp ... FAILED (ret code=1): 12/13 (replay failed) Replaying ./gcd ... FAILED (ret code=1): 11/13 (replay failed) Replaying ./gnome_sort ... FAILED (ret code=1): 0/1 (replay failed) Replaying ./knuth_prime_numbers ... FAILED (ret code=1): 1/3 (replay failed) Replaying ./my_cosine ... FAILED (ret code=1): 1/1 (replay failed) Replaying ./queens ... FAILED (ret code=1): 4/5 (replay failed) Replaying ./sieve ... FAILED (ret code=1): 2/2 (replay failed) Replaying ./space_saving ... FAILED (ret code=1): 5/6 (replay failed) Replaying ./there_and_back_again ... FAILED (ret code=1): 3/4 (replay failed) Replaying ./tortoise_and_hare ... FAILED (ret code=1): 4/5 (replay failed) Replaying ./vacid_0_red_black_trees ... FAILED (ret code=1): 36/37 (replay failed) Replaying ./vstte10_inverting ... FAILED (ret code=1): 1/3 (replay failed) Replaying ./vstte12_bfs ... FAILED (ret code=1): 5/6 (replay failed) Replaying ./vstte12_ring_buffer ... FAILED (ret code=1): 19/20 (replay failed) Replaying ./vstte12_tree_reconstruction ... FAILED (ret code=1): 20/23 (replay failed) Replaying vacid_0_binary_heaps/proofs ... FAILED (ret code=1): 37/38 (replay failed) Replaying verifythis_2016_matrix_multiplication/strassen ... FAILED (ret code=1): 13/14 (replay failed) Replaying WP_revisited/blocking_semantics5 ... FAILED (ret code=1): 36/38 (replay failed) Replaying WP_revisited/imp_n ... FAILED (ret code=1): 16/18 (replay failed) Replaying WP_revisited/wp2 ... FAILED (ret code=1): 25/30 (replay failed) Replaying prover/BacktrackArray ... FAILED (ret code=1): 7/8 (replay failed) Replaying multiprecision/add_1 ... FAILED (ret code=1): 3/4 (replay failed) Replaying multiprecision/div ... FAILED (ret code=1): 9/13 (replay failed) Replaying multiprecision/get_str ... FAILED (ret code=1): 2/4 (replay failed) Replaying multiprecision/lineardecision ... FAILED (ret code=1): 225/226 (replay failed) Replaying multiprecision/mpz_add ... FAILED (ret code=1): 0/2 (replay failed) Replaying multiprecision/mpz_div2exp ... FAILED (ret code=1): 2/3 (replay failed) Replaying multiprecision/mpz_div ... FAILED (ret code=1): 1/2 (replay failed) Replaying multiprecision/mpz_get_str ... FAILED (ret code=1): 2/3 (replay failed) Replaying multiprecision/mpz_mul2exp ... FAILED (ret code=1): 0/1 (replay failed) Replaying multiprecision/mpz_set_str ... FAILED (ret code=1): 0/1 (replay failed) Replaying multiprecision/powm ... FAILED (ret code=1): 16/18 (replay failed) Replaying multiprecision/set_str ... FAILED (ret code=1): 1/3 (replay failed) Replaying multiprecision/sqrtrem ... FAILED (ret code=1): 5/6 (replay failed) Replaying multiprecision/sqrt ... FAILED (ret code=1): 2/3 (replay failed) Replaying multiprecision/sub ... FAILED (ret code=1): 11/12 (replay failed) Replaying multiprecision/toom ... FAILED (ret code=1): 6/8 (replay failed) Replaying stdlib/array ... FAILED (ret code=1): 20/22 (replay failed) Replaying tests-provers/div ... FAILED (ret code=1): 13/25 (replay failed) Replaying tests-provers/ieee_float ... FAILED (ret code=1): 16/20 (replay failed) Replaying logic/genealogy ... FAILED (ret code=1): 7/7 (replay failed) Replaying logic/my_cosine ... FAILED (ret code=1): 4/4 (replay failed) Replaying bitvectors/double_of_int ... FAILED (ret code=1): 62/63 (replay failed) Replaying bitvectors/power2 ... FAILED (ret code=1): 84/85 (replay failed)
added 50 commits
-
16e4367c...a17ccaea - 49 commits from branch
master
- e9c92e49 - Merge branch 'master' into 417-internal-error-in-alt-ergo-after-inline_trivial
-
16e4367c...a17ccaea - 49 commits from branch
unassigned @pbonnot
Please register or sign in to reply