Ugly commit 1.

viperproject · Mar 20, 2023 · 445872f · 445872f
1 parent cf05ab9
commit 445872f
Showing 1 changed file with 23 additions and 22 deletions.
diff --git a/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs b/prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs
@@ -1101,6 +1101,19 @@ impl IntoLow for vir_mid::Statement {
                             false,
                             statement.position,
                         )?;
+                        let trigger_base = lowerer.unique_ref_range_snap(
+                            CallContext::Procedure,
+                            ty,
+                            target_type,
+                            start_address.clone(),
+                            base_index.clone(),
+                            end_index.clone(),
+                            lifetime.clone().into(),
+                            true,
+                            statement.position,
+                        )?;
+                        let snapshot_seq_type =
+                            vir_low::operations::ty::Typed::get_type(&current_snapshot).clone();
                         let label = lowerer.fresh_label("dead_reference_label")?;
                         lowerer.save_old_label(label.clone())?;
                         let current_snapshot = vir_low::Expression::labelled_old_no_pos(
@@ -1110,27 +1123,26 @@ impl IntoLow for vir_mid::Statement {
                         var_decls! {
                             index: Int
                         }
-                        let size_type = lowerer.size_type_mid()?;
-                        let base_index = lowerer.obtain_constant_value(
-                            &size_type,
-                            base_index,
+                        let trigger = vir_low::Expression::container_op(
+                            vir_low::ContainerOpKind::SeqIndex,
+                            snapshot_seq_type.clone(),
+                            vec![trigger_base, index.clone().into()],
                             statement.position,
-                        )?;
-                        let start_index = lowerer.obtain_constant_value(
+                        );
+                        let size_type = lowerer.size_type_mid()?;
+                        let start_index_int = lowerer.obtain_constant_value(
                             &size_type,
                             start_index,
                             statement.position,
                         )?;
-                        let end_index = lowerer.obtain_constant_value(
+                        let end_index_int = lowerer.obtain_constant_value(
                             &size_type,
                             end_index,
                             statement.position,
                         )?;
-                        let snapshot_seq_type =
-                            vir_low::operations::ty::Typed::get_type(&current_snapshot).clone();
                         let element_index = vir_low::Expression::subtract(
                             index.clone().into(),
-                            start_index.clone().into(),
+                            start_index_int.clone(),
                         );
                         let current_snapshot_element = vir_low::Expression::container_op(
                             vir_low::ContainerOpKind::SeqIndex,
@@ -1144,23 +1156,12 @@ impl IntoLow for vir_mid::Statement {
                             vec![final_snapshot, element_index],
                             statement.position,
                         );
-                        let trigger = lowerer.unique_ref_range_snap(
-                            CallContext::Procedure,
-                            ty,
-                            target_type,
-                            start_address.clone(),
-                            base_index.clone(),
-                            end_index.clone(),
-                            lifetime.clone().into(),
-                            true,
-                            statement.position,
-                        )?;
                         // We need this to ensure that Silicon does not complain
                         // that the trigger is invalid.
                         let trigger_validity =
                             lowerer.trigger_expression(trigger.clone(), statement.position)?;
                         let quantifier_body = expr! {
-                            (([start_index] <= index) && (index < [end_index])) ==>
+                            (([start_index_int] <= index) && (index < [end_index_int])) ==>
                             (
                                 ([trigger_validity]) &&
                                 ([current_snapshot_element] == [final_snapshot_element])