Remove a debug print, and use from_raw_span

Author: parno

verify/air/src/context.rs

@@ -238,10 +238,6 @@ impl<'ctx> Context<'ctx> {
             return ValidityResult::TypeError(err);
         }
         let (query, snapshots, local_vars) = crate::var_to_const::lower_query(query);
-
-        for (snap_id, _id_snapshot) in &snapshots {
-            println!("check_valid snap: {}", snap_id);
-        }
         self.air_middle_log.log_query(&query);
         let query = crate::block_to_assert::lower_query(&query);
         self.air_final_log.log_query(&query);

verify/rust_verify/src/model.rs

@@ -1,3 +1,4 @@
+use crate::util::from_raw_span;
 use air::ast::Ident;
 use air::ast::Span as ASpan;
 use rustc_span::source_map::SourceMap;
@@ -26,9 +27,7 @@ impl<'a> Model<'a> {
 
         if snap_map.len() > 0 {
             let (air_span, snap_pos) = &snap_map[0];
-            let span: &Span = (*air_span.raw_span)
-                .downcast_ref::<Span>()
-                .expect("internal error: failed to cast to Span");
+            let span: &Span = &from_raw_span(&air_span.raw_span);
             let (start, end) =
                 source_map.is_valid_span(*span).expect("internal error: invalid Span");
 
@@ -41,9 +40,7 @@ impl<'a> Model<'a> {
             let mut max_line = end.line;
 
             for (air_span, snap_pos) in snap_map {
-                let span: &Span = (*air_span.raw_span)
-                    .downcast_ref::<Span>()
-                    .expect("internal error: failed to cast to Span");
+                let span: &Span = &from_raw_span(&air_span.raw_span);
                 let (span_start, span_end) =
                     source_map.is_valid_span(*span).expect("internal error: invalid Span");
 
@@ -80,9 +77,7 @@ impl<'a> Model<'a> {
 
         // Debugging sanity checks
         for (air_span, snap_pos) in snap_map {
-            let span: &Span = (*air_span.raw_span)
-                .downcast_ref::<Span>()
-                .expect("internal error: failed to cast to Span");
+            let span: &Span = &from_raw_span(&air_span.raw_span);
             let (start, end) =
                 source_map.is_valid_span(*span).expect("internal error: invalid Span");
             println!("Span from {} to {} => {:?}", start.line, end.line, snap_pos);