Resolve "Internal error in Alt-ergo after inline_trivial"

Closes #417

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

Compare with previous version

added 1 commit

• efdda7b6 - Added examples

Compare with previous version

marked this merge request as ready

added 1 commit

• cc1b98d4 - Moved the meta to stdlib

Compare with previous version

added 1 commit

• 6220613a - Update oracles

Compare with previous version

added 1 commit

• 66ab3db7 - update realizations, in progress

Compare with previous version

added 1 commit

• 032d1815 - more Coq proofs

Compare with previous version

mentioned in merge request !875 (merged)

added 1 commit

• 65d88c3d - Updated realizations

Compare with previous version

added 1 commit

• e0a4b11f - wip

Compare with previous version

added 1 commit

• 6134c39a - Revert "Updated realizations"

Compare with previous version

added 1 commit

• b9ed009b - Coq realizations OK

Compare with previous version

removed To be discussed label

added ProofInUse/TrustInSoft label

Thanks for updating Coq proofs. It seems it fails now in compiling Abs.v, strange, to be investigated

It seems the proof is OK for Coq 8.16, but not for Coq 8.11. Annoying!

It works also for version 8.13. Time to update Coq on Molloch ? :)

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

Compare with previous version

added 1 commit

• 16e4367c - diff in bench-api directly copied into oracle

Compare with previous version

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

Compare with previous version

unassigned @pbonnot