Entered unreachable code in `Expr::has_prefix`

[fpoli]

The following program crashes while encoding test with an "internal error: entered unreachable code: 1" in vir_gen.rs.

Backtrace

[2022-03-24T10:14:30Z INFO  prusti_viper::encoder::encoder] Encoding: 20220324_110509::test (20220324_110509::test)
thread 'rustc' panicked at 'internal error: entered unreachable code: 1', vir/src/../gen/vir_gen.rs:40651:34
stack backtrace:
   0: rust_begin_unwind
             at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
   1: core::panicking::panic_fmt
             at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
   2: vir::gen::polymorphic::ast::expr::Expr::has_prefix
   3: vir::gen::polymorphic::ast::expr::Expr::has_prefix
   4: vir::gen::polymorphic::ast::expr::Expr::has_prefix
   5: prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain
   6: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::try_fold
   7: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
   8: core::iter::adapters::try_process
   9: prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain_permissions
  10: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold
  11: vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed
  12: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold_labelled_old
  13: vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr
  14: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold
  15: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::try_fold
  16: alloc::vec::source_iter_marker::<impl alloc::vec::spec_from_iter::SpecFromIter<T,I> for alloc::vec::Vec<T>>::from_iter
  17: core::iter::adapters::try_process
  18: vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_func_app
  19: vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr
  20: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold
  21: vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed
  22: vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr
  23: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold
  24: vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed
  25: vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr
  26: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold
  27: vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed
  28: vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_bin_op
  29: vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr
  30: <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold
  31: vir::gen::polymorphic::ast::stmt::FallibleStmtFolder::fallible_fold
  32: prusti_viper::encoder::foldunfold::FoldUnfold::rewrite_stmt_with_unfoldings_in_old
  33: <prusti_viper::encoder::foldunfold::FoldUnfold as vir::gen::polymorphic::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt,prusti_viper::encoder::foldunfold::ActionVec>>::replace_stmt
  34: prusti_viper::encoder::foldunfold::add_fold_unfold
  35: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
  36: prusti_viper::encoder::encoder::Encoder::encode_procedure
  37: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
  38: prusti_viper::verifier::Verifier::verify
  39: prusti_driver::verifier::verify
  40: rustc_interface::passes::QueryContext::enter
  41: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
  42: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
  43: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::create_compiler_and_run<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#1}>
  44: rustc_interface::interface::create_compiler_and_run::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>
  45: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

use prusti_contracts::*;
use std::collections::HashSet;
use std::hash::Hash;
use std::cmp::Eq;

struct SetWrapper<T: Hash + Eq> {
    set: HashSet<T>
}

impl<T: Hash + Eq> SetWrapper<T> {
    #[pure]
    #[trusted]
    pub fn contains(&self, value: &T) -> bool {
        self.set.contains(value)
    }

    #[ensures(self.contains(old(&value)))]
    pub fn insert(&mut self, value: T) {
        self.set.insert(value);
    }

    #[ensures(!self.contains(old(&value)))]
    pub fn remove(&mut self, value: &T) -> bool {
        self.set.remove(value)
    }
}

fn test() {
    let mut set = SetWrapper { set: HashSet::new() };
    set.insert(1);
    set.insert(2);
    set.insert(3);
    let one = 1;
    let two = 2;
    let three = 3;
    set.remove(&three);
    set.remove(&two);
    set.remove(&one);
    set.remove(&one);
}

fn main() {}