Mentions légales du service

Skip to content
Snippets Groups Projects

Resolve "Internal error in Alt-ergo after inline_trivial"

Closes #417

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • BONNOT Paul requested review from @marche

    requested review from @marche

  • assigned to @pbonnot

  • BONNOT Paul added 1 commit

    added 1 commit

    • f170b391 - Changed alt-ergo drivers so that we don't unfold basic arithmetic symbols

    Compare with previous version

  • BONNOT Paul added 1 commit

    added 1 commit

    Compare with previous version

  • BONNOT Paul marked this merge request as ready

    marked this merge request as ready

  • BONNOT Paul added 1 commit

    added 1 commit

    Compare with previous version

  • BONNOT Paul added 1 commit

    added 1 commit

    Compare with previous version

  • MARCHE Claude added 1 commit

    added 1 commit

    • 66ab3db7 - update realizations, in progress

    Compare with previous version

  • MARCHE Claude added 1 commit

    added 1 commit

    Compare with previous version

  • MARCHE Claude mentioned in merge request !875 (merged)

    mentioned in merge request !875 (merged)

  • BONNOT Paul added 1 commit

    added 1 commit

    Compare with previous version

  • BONNOT Paul added 1 commit

    added 1 commit

    • 6134c39a - Revert "Updated realizations"

    Compare with previous version

  • BONNOT Paul added 1 commit

    added 1 commit

    Compare with previous version

  • 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!

  • Author Developer

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

  • MARCHE Claude added 51 commits

    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

  • MARCHE Claude added 1 commit

    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)
  • BONNOT Paul added 50 commits

    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

Please register or sign in to reply
Loading