Ugly commit.

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/mod.rs

@@ -12,6 +12,7 @@ use super::{
     trace_builder::{ExecutionTraceBuilder, ExecutionTraceHeapView},
     VerificationResult,
 };
+use log::debug;
 use rustc_hash::FxHashMap;
 use std::collections::BTreeMap;
 use vir_crate::{
@@ -144,7 +145,7 @@ impl ExecutionTraceBuilder {
         &self,
         program: &ProgramContext,
     ) -> VerificationResult<Trace> {
-        eprintln!("Finalizing trace");
+        debug!("Finalizing trace");
         let (state, solver) = self.current_heap_and_egraph_state();
         let view = self.heap_view();
         let last_block_id = view.last_block_id();

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/predicate_snapshots.rs

@@ -20,12 +20,16 @@ impl PredicateSnapshots {
         let predicate_snapshots = self.snapshots.entry(predicate.name.clone()).or_default();
         let snapshot_variable_name =
             format!("snapshot${}${}", predicate.name, predicate_snapshots.len());
-        let ty = program_context.get_snapshot_type(&predicate.name).unwrap();
-        let snapshot = vir_low::VariableDecl::new(snapshot_variable_name, ty);
-        self.variables.push(snapshot.clone());
+        let snapshot = if let Some(ty) = program_context.get_snapshot_type(&predicate.name) {
+            let snapshot = vir_low::VariableDecl::new(snapshot_variable_name, ty);
+            self.variables.push(snapshot.clone());
+            PredicateSnapshotState::Inhaled(snapshot)
+        } else {
+            PredicateSnapshotState::NoSnapshot
+        };
         predicate_snapshots.push(PredicateSnapshot {
             arguments: predicate.arguments.clone(),
-            snapshot: Some(snapshot),
+            snapshot,
         });
     }
 
@@ -36,10 +40,10 @@ impl PredicateSnapshots {
     ) -> VerificationResult<()> {
         let predicate_snapshots = self.snapshots.get_mut(&predicate.name).unwrap();
         for predicate_snapshot in predicate_snapshots {
-            if predicate_snapshot.snapshot.is_some()
+            if predicate_snapshot.snapshot.is_not_exhaled()
                 && predicate_snapshot.matches(predicate, solver)?
             {
-                predicate_snapshot.snapshot = None;
+                predicate_snapshot.snapshot = PredicateSnapshotState::Exhaled;
             }
         }
         Ok(())
@@ -53,7 +57,7 @@ impl PredicateSnapshots {
     ) -> VerificationResult<Option<vir_low::VariableDecl>> {
         if let Some(predicate_snapshots) = self.snapshots.get(predicate_name) {
             for predicate_snapshot in predicate_snapshots {
-                if let Some(snapshot) = &predicate_snapshot.snapshot {
+                if let PredicateSnapshotState::Inhaled(snapshot) = &predicate_snapshot.snapshot {
                     if predicate_snapshot.matches_arguments(arguments, solver)? {
                         return Ok(Some(snapshot.clone()));
                     }
@@ -68,12 +72,31 @@ impl PredicateSnapshots {
     }
 }
 
+#[derive(Clone)]
+enum PredicateSnapshotState {
+    /// The snapshot is valid.
+    Inhaled(vir_low::VariableDecl),
+    /// The snapshot was exhaled and no longer valid.
+    Exhaled,
+    /// The predicate does not have a snapshot.
+    NoSnapshot,
+}
+
+impl PredicateSnapshotState {
+    pub(super) fn is_not_exhaled(&self) -> bool {
+        matches!(
+            self,
+            PredicateSnapshotState::Inhaled(_) | PredicateSnapshotState::NoSnapshot
+        )
+    }
+}
+
 #[derive(Clone)]
 pub(super) struct PredicateSnapshot {
     /// Predicate arguments.
     arguments: Vec<vir_low::Expression>,
     /// None means that the corresponding predicate was exhaled.
-    snapshot: Option<vir_low::VariableDecl>,
+    snapshot: PredicateSnapshotState,
 }
 
 impl PredicateSnapshot {

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/mod.rs

@@ -16,6 +16,7 @@ use self::{egg::EGraphState, program_context::ProgramContext};
 use crate::encoder::{
     errors::SpannedEncodingResult, middle::core_proof::predicates::PredicateInfo,
 };
+use log::debug;
 use prusti_common::config;
 use rustc_hash::FxHashMap;
 use std::collections::BTreeMap;
@@ -137,7 +138,7 @@ impl<'a> ProcedureExecutor<'a> {
         procedure: vir_low::ProcedureDecl,
         new_procedures: &mut Vec<vir_low::ProcedureDecl>,
     ) -> VerificationResult<()> {
-        eprintln!("Executing procedure {}", procedure.name);
+        debug!("Executing procedure {}", procedure.name);
         let mut current_block = procedure.entry.clone();
         loop {
             let block = procedure.basic_blocks.get(&current_block).unwrap();
@@ -248,7 +249,7 @@ impl<'a> ProcedureExecutor<'a> {
         default_position: vir_low::Position,
     ) -> VerificationResult<Option<vir_low::Label>> {
         while let Some(continuation) = self.continuations.pop() {
-            eprintln!("Rolling back to {}", continuation.parent_block_label);
+            debug!("Rolling back to {}", continuation.parent_block_label);
             self.execution_trace_builder
                 .rollback_to_split_point(continuation.parent_block_label)?;
             self.assume_condition(continuation.condition, default_position)?;
@@ -257,7 +258,7 @@ impl<'a> ProcedureExecutor<'a> {
                 .current_egraph_state()
                 .is_inconsistent()?
             {
-                eprintln!("Inconsistent after rollback");
+                debug!("Inconsistent after rollback");
                 self.execution_trace_builder.remove_last_block()?;
             } else {
                 return Ok(Some(continuation.next_block_label));
@@ -286,7 +287,7 @@ impl<'a> ProcedureExecutor<'a> {
         current_block: &vir_low::Label,
         block: &vir_low::BasicBlock,
     ) -> VerificationResult<()> {
-        eprintln!("Executing block {}", current_block);
+        debug!("Executing block {}", current_block);
         for statement in &block.statements {
             self.execute_statement(current_block, statement)?;
         }

prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/mod.rs

@@ -149,9 +149,6 @@ impl ExecutionTraceBuilder {
         };
         self.finalize_original_trace_for_block(&mut original_trace, self.blocks.len() - 1)?;
         let final_trace = self.heap_finalize_trace(program)?;
-        for v in &final_trace.variables {
-            eprintln!("final trace variable: {}", v);
-        }
         Ok((original_trace, final_trace))
     }