Ugly commit 26.13.

prusti-viper/src/encoder/high/procedures/inference/eval_using.rs

@@ -19,7 +19,7 @@ pub(super) fn wrap_in_eval_using(
     state: &mut super::state::FoldUnfoldState,
     mut expression: vir_typed::Expression,
 ) -> SpannedEncodingResult<vir_typed::Expression> {
-    let accessed_places = strip_dereferences(expression.collect_all_places());
+    let accessed_places = strip_dereferences(expression.collect_all_places_with_old_locals());
     let mut framing_places = Vec::new();
     let mut context_kinds = Vec::new();
     for accessed_place in accessed_places {
@@ -32,6 +32,10 @@ pub(super) fn wrap_in_eval_using(
                 _ => vir_typed::EvalInContextKind::OldOpenedRefPredicate,
             };
             if !framing_places.contains(old_wrap) {
+                // FIXME: We should look up the actual state of the place in the
+                // old state instead of just assuming that it is fully folded
+                // (which works most of the time because old refers to
+                // preconditions).
                 framing_places.push(old_wrap.clone());
                 context_kinds.push(context_kind);
             }

prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/assertions/self_framing.rs

@@ -459,6 +459,34 @@ impl<'p, 'v: 'p, 'tcx: 'v> IntoSnapshotLowerer<'p, 'v, 'tcx> for SelfFramingAsse
         self.expression_to_snapshot_impl(lowerer, expression, expect_math_bool)
     }
 
+    fn local_to_snapshot(
+        &mut self,
+        lowerer: &mut Lowerer<'p, 'v, 'tcx>,
+        local: &vir_mid::Local,
+        expect_math_bool: bool,
+    ) -> SpannedEncodingResult<vir_low::Expression> {
+        if let Some(label) = &self.old_label {
+            for (place, call) in &self.snap_calls {
+                if let vir_mid::Expression::LabelledOld(vir_mid::LabelledOld {
+                    label: old_label,
+                    base: box vir_mid::Expression::Local(predicate_local),
+                    ..
+                }) = place
+                {
+                    if old_label == label && predicate_local == local {
+                        return self.ensure_bool_expression(
+                            lowerer,
+                            local.get_type(),
+                            call.clone(),
+                            expect_math_bool,
+                        );
+                    }
+                }
+            }
+        }
+        self.local_to_snapshot_impl(lowerer, local, expect_math_bool)
+    }
+
     fn binary_op_to_snapshot(
         &mut self,
         lowerer: &mut Lowerer<'p, 'v, 'tcx>,

prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs

@@ -157,6 +157,15 @@ pub(in super::super::super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v>:
         lowerer: &mut Lowerer<'p, 'v, 'tcx>,
         local: &vir_mid::Local,
         expect_math_bool: bool,
+    ) -> SpannedEncodingResult<vir_low::Expression> {
+        self.local_to_snapshot_impl(lowerer, local, expect_math_bool)
+    }
+
+    fn local_to_snapshot_impl(
+        &mut self,
+        lowerer: &mut Lowerer<'p, 'v, 'tcx>,
+        local: &vir_mid::Local,
+        expect_math_bool: bool,
     ) -> SpannedEncodingResult<vir_low::Expression> {
         let snapshot_variable = self.variable_to_snapshot(lowerer, &local.variable)?;
         let result = vir_low::Expression::local(snapshot_variable, local.position);

vir/defs/high/operations_internal/expression.rs

@@ -177,30 +177,55 @@ impl Expression {
             _ => false,
         }
     }
-    pub fn collect_all_places(&self) -> Vec<Expression> {
+    /// Returns all places:
+    ///
+    /// * If a place is not inside `old`, then it is returned as it is.
+    /// * If a place is inside `old`, then it is returned as `old(variable)`.
+    pub fn collect_all_places_with_old_locals(&self) -> Vec<Expression> {
         struct Collector {
             // We use `Vec` instead of `HashSet` to make sure we are
             // deterministic.
             places: Vec<Expression>,
+            old_label: Option<String>,
         }
         impl ExpressionWalker for Collector {
             fn walk_expression(&mut self, expression: &Expression) {
-                if expression.is_place() {
+                if self.old_label.is_none() && expression.is_place() {
                     self.places.push(expression.clone());
                 } else {
                     default_walk_expression(self, expression)
                 }
             }
+            fn walk_local(&mut self, local: &Local) {
+                let Some(label) = &self.old_label else {
+                    unreachable!("something went wrong; this should be reachable only with old set");
+                };
+                let position = local.position;
+                self.places.push(Expression::labelled_old(
+                    label.clone(),
+                    Expression::Local(local.clone()),
+                    position,
+                ));
+            }
             fn walk_predicate(&mut self, predicate: &Predicate) {
                 PredicateWalker::walk_predicate(self, predicate)
             }
+            fn walk_labelled_old(&mut self, labelled_old: &LabelledOld) {
+                let old_label =
+                    std::mem::replace(&mut self.old_label, Some(labelled_old.label.clone()));
+                ExpressionWalker::walk_expression(self, &labelled_old.base);
+                self.old_label = old_label;
+            }
         }
         impl PredicateWalker for Collector {
             fn walk_expression(&mut self, expr: &Expression) {
                 ExpressionWalker::walk_expression(self, expr)
             }
         }
-        let mut collector = Collector { places: Vec::new() };
+        let mut collector = Collector {
+            places: Vec::new(),
+            old_label: None,
+        };
         ExpressionWalker::walk_expression(&mut collector, self);
         collector.places
     }