Disabled tests

[Aurel300]

This is a tracking issue for tests that are currently disabled, either with // ignore-test or by being placed in the tests_old directory. Please edit this issue if the list is changed and state the reason and any related issues or PRs.

---

tests_old

• fails during fold/unfold or panics with "Location bb5[6] has not yet been encoded"
  • tests_old/filter/fail_reborrowing{,_2,_3,_4}.rs
• after Cleanup snapshot encoding #402, for these we need better recursive pure functions (manual axiomatisation)
  • tests_old/verify/fail/demos/append-sorted-error-{1,2,4}.rs
  • tests_old/verify/pass/demos/append-sorted.rs
  • tests_old/verify/pass/gitlab-issues/issue-187-1.rs
  • tests_old/verify/pass/paper-examples/force_increasing.rs
  • tests_old/verify/pass/quick/with-spec-list.rs (also has a fold/unfold issue)
• too slow/need purification optimisation
  • tests_old/verify/pass/competitive_programming/*
• unsupported feature: "unsupported creation of shallow borrows (implicitly created when lowering matches)" (although all other expected errors are found)
  • tests_old/verify/fail/simple-specs/order-of-branches.rs
• remaining snapshot issues? "Consistency error: expected the same type, but got Ref and Snap$m_A$beg$end"
  • tests_old/verify/pass/equality/pure-first-arg.rs
  • tests_old/verify/pass/equality/pure-identity-main.rs
  • tests_old/verify/pass/equality/pure-impure-3.rs
  • tests_old/verify/pass/equality/pure-post-4.rs
• returning a non-Copy value from a pure function - maybe we don't actually want to support this?
  • tests_old/verify/pass/equality/pure-identity.rs
• fails fold/unfold
  • tests_old/verify/pass/expiring-loans/borrow-join.rs
  • tests_old/verify/pass/expiring-loans/return_borrow.rs
  • tests_old/verify/pass/expiring-loans/use_returned_borrow.rs
• non-linear arithmetic
  • tests_old/verify/pass/loop-invs/sum.rs
• type invariants and typestates not (re)implemented
  • tests_old/verify/fail/erdinm/invariants-*.rs
  • tests_old/verify/fail/erdinm/typestates-*.rs
  • tests_old/verify/fail/marker-traits/*.rs
  • tests_old/verify/pass/erdinm/invariants-*.rs
  • tests_old/verify/pass/erdinm/typestates-basic-1.rs
  • tests_old/verify/pass/marker-traits/*.rs
  • tests_old/verify/pass/quick/marker-traits.rs
• assert_on_expiry
  • tests_old/verify/fail/erdinm/assert-on-expiry.rs
  • tests_old/verify/failerdinm/pledges-basic-*.rs
• trait refinement, refine_requires
  • tests_old/verify/fail/trait-contracts-refinement/*.rs
  • tests_old/verify/pass/erdinm/pledges-basic-*.rs
  • tests_old/verify/pass/unsafe-traits/*.rs
• insufficient permission to assert postcondition?
  • tests_old/verify/pass/generic/linear_search.rs

ignore-test

• pending on a new closure PR
  • tests/verify/pass/closures/*.rs
• issues with generics and pure functions (generates a duplicate method)
  • tests/verify/pass/extern-spec/linked-list-i32.rs
  • tests/verify/pass/extern-spec/vec-3.rs
• old(x) should produce a snapshot of x, not implemented
  • tests/verify/pass/gitlab-issues/issue-46-old-expr.rs
• magic wands in loop invariants
  • tests/verify/pass/loop-invs/borrow_in_guard.rs
  • tests/verify/pass/loop-invs/for_iter.rs
  • tests/verify/pass/loop-invs/simple_iterator.rs
• flaky tests (non-linear arithmetic)
  • tests/verify/pass/quick/knapsack.rs
  • tests/verify/pass/quick/mut-borrows-binary-search.rs

[fpoli]

Minus one 🎉

[fpoli]

verify_overflow/pass/rosetta /Knights_tour_generic.rs is disabled too because it was flaky due to random verification timeouts.