diff --git a/crates/filament/src/ir_passes/bundle_elim.rs b/crates/filament/src/ir_passes/bundle_elim.rs
index 57e16c96..ac4f144b 100644
--- a/crates/filament/src/ir_passes/bundle_elim.rs
+++ b/crates/filament/src/ir_passes/bundle_elim.rs
@@ -3,9 +3,9 @@ use crate::{
     ir_visitor::{Action, Construct, Visitor, VisitorData},
 };
 use fil_ir::{
-    self as ir, Access, AddCtx, Bind, Command, Component, Connect, Ctx,
-    DenseIndexInfo, DisplayCtx, Expr, Foreign, Info, InvIdx, Invoke, Liveness,
-    MutCtx, Port, PortIdx, PortOwner, Range, SparseInfoMap, Subst, Time,
+    self as ir, Access, AddCtx, Bind, Component, Connect, Ctx, DenseIndexInfo,
+    DisplayCtx, Expr, Foreign, InvIdx, Invoke, Liveness, MutCtx, Port, PortIdx,
+    PortOwner, Range, SparseInfoMap, Subst, Time,
 };
 use fil_utils as utils;
 use itertools::Itertools;
@@ -147,12 +147,26 @@ impl BundleElim {
                 let info = comp.add(info.clone());
 
                 // adds the new port to the component and return its index
-                comp.add(Port {
+                let pidx = comp.add(Port {
                     live,
                     owner,
                     info, // duplicate the info
                     width,
-                })
+                });
+
+                // Fill in the live idxs with a new dummy index
+                let port = ir::Param {
+                    owner: ir::ParamOwner::bundle(pidx),
+                    info: comp.add(ir::Info::param(
+                        "_".into(),
+                        utils::GPosIdx::UNKNOWN,
+                    )),
+                };
+                let port = comp.add(port);
+
+                comp.get_mut(pidx).live.idxs.push(port);
+
+                pidx
             })
             .collect();
         // delete the original port
@@ -228,7 +242,7 @@ impl Visitor for BundleElim {
         connect: &mut Connect,
         data: &mut VisitorData,
     ) -> Action {
-        let Connect { src, dst, .. } = connect;
+        let Connect { src, dst, info } = connect;
 
         if !self.context.get(data.idx).contains(dst.port) {
             // we are writing to a local port here.
@@ -253,11 +267,12 @@ impl Visitor for BundleElim {
             src.into_iter()
                 .zip_eq(dst)
                 .map(|(src, dst)| {
-                    Command::Connect(Connect {
+                    Connect {
                         src: Access::port(src, &mut data.comp),
                         dst: Access::port(dst, &mut data.comp),
-                        info: data.comp.add(Info::empty()),
-                    })
+                        info: *info,
+                    }
+                    .into()
                 })
                 .collect(),
         )
diff --git a/crates/filament/src/ir_passes/discharge.rs b/crates/filament/src/ir_passes/discharge.rs
index a14986f0..ea22d4b4 100644
--- a/crates/filament/src/ir_passes/discharge.rs
+++ b/crates/filament/src/ir_passes/discharge.rs
@@ -74,12 +74,12 @@ pub struct Discharge {
     /// Defined functions for `some` parameters on components
     comp_param_map: HashMap<ir::Foreign<ir::Param, ir::Component>, smt::SExpr>,
 
-    // Defined names
-    param_map: ir::DenseIndexInfo<ir::Param, smt::SExpr>,
-    ev_map: ir::DenseIndexInfo<ir::Event, smt::SExpr>,
+    // Defined names. These are sparse in case certain parameters or events have been invalidated.
+    param_map: ir::SparseInfoMap<ir::Param, smt::SExpr>,
+    ev_map: ir::SparseInfoMap<ir::Event, smt::SExpr>,
     // Composite expressions
-    expr_map: ir::DenseIndexInfo<ir::Expr, smt::SExpr>,
-    time_map: ir::DenseIndexInfo<ir::Time, smt::SExpr>,
+    expr_map: ir::SparseInfoMap<ir::Expr, smt::SExpr>,
+    time_map: ir::SparseInfoMap<ir::Time, smt::SExpr>,
     // Propositions
     prop_map: ir::DenseIndexInfo<ir::Prop, SExprWrapper>,
     // Propositions that have already been checked
@@ -609,7 +609,12 @@ impl Visitor for Discharge {
 
         let bs = self.sol.bool_sort();
         // Declare all expressions
-        for (idx, expr) in data.comp.exprs().iter() {
+        for (idx, expr) in data
+            .comp
+            .exprs()
+            .iter()
+            .filter(|(idx, _)| idx.valid(&data.comp))
+        {
             // do props inside of exprs ahead of time
             let relevant_props = idx
                 .relevant_props(&data.comp)
@@ -646,18 +651,31 @@ impl Visitor for Discharge {
         }
 
         // Declare all time expressions
-        for (idx, ir::Time { event, offset }) in data.comp.times().iter() {
-            let assign = self.plus(self.ev_map[*event], self.expr_map[*offset]);
-            let sexp = self
-                .sol
-                .define_const(Self::fmt_time(idx), int, assign)
-                .unwrap();
-            self.overflow_assert(sexp);
-            self.time_map.push(idx, sexp);
+        for (idx, ir::Time { event, offset }) in data
+            .comp
+            .times()
+            .iter()
+            .filter(|(idx, _)| idx.valid(&data.comp))
+        {
+            if self.ev_map.contains(*event) && self.expr_map.contains(*offset) {
+                let assign =
+                    self.plus(self.ev_map[*event], self.expr_map[*offset]);
+                let sexp = self
+                    .sol
+                    .define_const(Self::fmt_time(idx), int, assign)
+                    .unwrap();
+                self.overflow_assert(sexp);
+                self.time_map.push(idx, sexp);
+            }
         }
 
         // Declare all propositions
-        for (idx, prop) in data.comp.props().iter() {
+        for (idx, prop) in data
+            .comp
+            .props()
+            .iter()
+            .filter(|(idx, _)| idx.valid(&data.comp))
+        {
             // Define assertion equating the proposition to its assignment
             let assign = self.prop_to_sexp(prop);
             if let Ok(sexp) =
diff --git a/crates/filament/src/main.rs b/crates/filament/src/main.rs
index c49d7116..e6ca3b6a 100644
--- a/crates/filament/src/main.rs
+++ b/crates/filament/src/main.rs
@@ -97,6 +97,17 @@ fn run(opts: &cmdline::Opts) -> Result<(), u64> {
         ip::BundleElim,
         ip::AssignCheck
     }
+    // type check again before lowering
+    ir_pass_pipeline! {opts, ir;
+        ip::BuildDomination,
+        ip::TypeCheck,
+        ip::IntervalCheck,
+        ip::PhantomCheck,
+        ip::Assume
+    }
+    if !opts.unsafe_skip_discharge {
+        ir_pass_pipeline! {opts, ir; ip::Discharge }
+    }
 
     // Return early if we're asked to dump the interface
     if opts.dump_interface {
diff --git a/crates/ir/src/expr.rs b/crates/ir/src/expr.rs
index d7b6fc04..1fdec817 100644
--- a/crates/ir/src/expr.rs
+++ b/crates/ir/src/expr.rs
@@ -1,5 +1,5 @@
-use super::{AddCtx, Component, Ctx, ExprIdx, ParamIdx};
-use crate::{construct_binop, Prop, PropIdx};
+use super::{AddCtx, Component, Ctx, ExprIdx, MutCtx, ParamIdx};
+use crate::{construct_binop, Param, Prop, PropIdx};
 use fil_ast as ast;
 use std::fmt::Display;
 
@@ -112,20 +112,26 @@ impl ExprIdx {
 
 /// Queries over [ExprIdx]
 impl ExprIdx {
-    pub fn relevant_props(
-        &self,
-        ctx: &(impl Ctx<Expr> + Ctx<Prop>),
-    ) -> Vec<PropIdx> {
+    pub fn valid<C>(&self, ctx: &C) -> bool
+    where
+        C: Ctx<Expr> + Ctx<Prop> + MutCtx<Param>,
+    {
+        self.relevant_vars(ctx).iter().all(|p| ctx.valid(*p))
+    }
+
+    pub fn relevant_props<C>(&self, ctx: &C) -> Vec<PropIdx>
+    where
+        C: Ctx<Expr> + Ctx<Prop>,
+    {
         let mut props = Vec::new();
         self.relevant_props_acc(ctx, &mut props);
         props
     }
 
-    pub fn relevant_props_acc(
-        &self,
-        ctx: &(impl Ctx<Expr> + Ctx<Prop>),
-        props: &mut Vec<PropIdx>,
-    ) {
+    pub fn relevant_props_acc<C>(&self, ctx: &C, props: &mut Vec<PropIdx>)
+    where
+        C: Ctx<Expr> + Ctx<Prop>,
+    {
         if let Expr::If { cond, .. } = ctx.get(*self) {
             props.push(*cond);
             let inner_props = cond.relevant_props(ctx);
@@ -133,20 +139,19 @@ impl ExprIdx {
         }
     }
 
-    pub fn relevant_vars(
-        &self,
-        ctx: &(impl Ctx<Expr> + Ctx<Prop>),
-    ) -> Vec<ParamIdx> {
+    pub fn relevant_vars<C>(&self, ctx: &C) -> Vec<ParamIdx>
+    where
+        C: Ctx<Expr> + Ctx<Prop>,
+    {
         let mut params = Vec::new();
         self.relevant_vars_acc(ctx, &mut params);
         params
     }
 
-    pub fn relevant_vars_acc(
-        &self,
-        ctx: &(impl Ctx<Expr> + Ctx<Prop>),
-        params: &mut Vec<ParamIdx>,
-    ) {
+    pub fn relevant_vars_acc<C>(&self, ctx: &C, params: &mut Vec<ParamIdx>)
+    where
+        C: Ctx<Expr> + Ctx<Prop>,
+    {
         match ctx.get(*self) {
             Expr::Param(p) => {
                 params.push(*p);
diff --git a/crates/ir/src/fact.rs b/crates/ir/src/fact.rs
index c11981c0..5a1bb588 100644
--- a/crates/ir/src/fact.rs
+++ b/crates/ir/src/fact.rs
@@ -1,5 +1,7 @@
-use super::{idxs::PropIdx, AddCtx, Ctx, ExprIdx, InfoIdx, TimeIdx, TimeSub};
-use crate::{construct_binop, EventIdx, Expr, ParamIdx, Time};
+use super::{
+    idxs::PropIdx, AddCtx, Ctx, ExprIdx, InfoIdx, MutCtx, TimeIdx, TimeSub,
+};
+use crate::{construct_binop, Event, EventIdx, Expr, Param, ParamIdx, Time};
 use std::fmt::{self, Display};
 
 #[derive(Clone, PartialEq, Eq, Hash)]
@@ -233,11 +235,13 @@ impl PropIdx {
     }
 
     // relevant vars of an if guard -- can't include times
-    pub fn relevant_vars_if_acc(
+    pub fn relevant_vars_if_acc<C>(
         &self,
-        ctx: &(impl Ctx<Prop> + Ctx<Expr>),
+        ctx: &C,
         param_acc: &mut Vec<ParamIdx>,
-    ) {
+    ) where
+        C: Ctx<Prop> + Ctx<Expr>,
+    {
         match ctx.get(*self) {
             Prop::True | Prop::False => (),
             Prop::Cmp(CmpOp { lhs, rhs, .. }) => {
@@ -256,12 +260,14 @@ impl PropIdx {
     }
 
     /// Accumulate all the parameters and events that appear in this proposition.
-    pub fn relevant_vars_acc(
+    pub fn relevant_vars_acc<C>(
         &self,
-        ctx: &(impl Ctx<Prop> + Ctx<Time> + Ctx<Expr>),
+        ctx: &C,
         param_acc: &mut Vec<ParamIdx>,
         event_acc: &mut Vec<EventIdx>,
-    ) {
+    ) where
+        C: Ctx<Prop> + Ctx<Time> + Ctx<Expr>,
+    {
         let mut time_acc = |time: TimeIdx, params: &mut Vec<ParamIdx>| {
             let Time { event, offset } = ctx.get(time);
             event_acc.push(*event);
@@ -302,39 +308,38 @@ impl PropIdx {
 
     /// Returns the parameters and events mentioned in the proposition.
     #[inline]
-    pub fn relevant_vars(
-        &self,
-        ctx: &(impl Ctx<Time> + Ctx<Prop> + Ctx<Expr>),
-    ) -> (Vec<ParamIdx>, Vec<EventIdx>) {
+    pub fn relevant_vars<C>(&self, ctx: &C) -> (Vec<ParamIdx>, Vec<EventIdx>)
+    where
+        C: Ctx<Time> + Ctx<Prop> + Ctx<Expr>,
+    {
         let mut params = Vec::new();
         let mut events = Vec::new();
         self.relevant_vars_acc(ctx, &mut params, &mut events);
         (params, events)
     }
 
-    pub fn relevant_vars_if(
-        &self,
-        ctx: &(impl Ctx<Prop> + Ctx<Expr>),
-    ) -> Vec<ParamIdx> {
+    pub fn relevant_vars_if<C>(&self, ctx: &C) -> Vec<ParamIdx>
+    where
+        C: Ctx<Prop> + Ctx<Expr>,
+    {
         let mut params = Vec::new();
         self.relevant_vars_if_acc(ctx, &mut params);
         params
     }
 
-    pub fn relevant_props(
-        &self,
-        ctx: &(impl Ctx<Prop> + Ctx<Expr>),
-    ) -> Vec<PropIdx> {
+    pub fn relevant_props<C>(&self, ctx: &C) -> Vec<PropIdx>
+    where
+        C: Ctx<Prop> + Ctx<Expr>,
+    {
         let mut props = Vec::new();
         self.relevant_props_acc(ctx, &mut props);
         props
     }
 
-    pub fn relevant_props_acc(
-        &self,
-        ctx: &(impl Ctx<Prop> + Ctx<Expr>),
-        props: &mut Vec<PropIdx>,
-    ) {
+    pub fn relevant_props_acc<C>(&self, ctx: &C, props: &mut Vec<PropIdx>)
+    where
+        C: Ctx<Prop> + Ctx<Expr>,
+    {
         match ctx.get(*self) {
             Prop::True | Prop::False => (),
             Prop::Cmp(CmpOp { lhs, rhs, .. }) => {
@@ -357,6 +362,15 @@ impl PropIdx {
             }
         }
     }
+
+    pub fn valid<C>(&self, ctx: &C) -> bool
+    where
+        C: Ctx<Prop> + Ctx<Time> + Ctx<Expr> + MutCtx<Param> + MutCtx<Event>,
+    {
+        let (props, events) = self.relevant_vars(ctx);
+        props.iter().all(|p| ctx.valid(*p))
+            && events.iter().all(|e| ctx.valid(*e))
+    }
 }
 
 #[derive(Clone, PartialEq, Eq)]
diff --git a/crates/ir/src/time.rs b/crates/ir/src/time.rs
index e4d6093a..8b4aa7dc 100644
--- a/crates/ir/src/time.rs
+++ b/crates/ir/src/time.rs
@@ -1,4 +1,4 @@
-use crate::{DisplayCtx, Prop};
+use crate::{DisplayCtx, MutCtx, Param, Prop};
 
 use super::{
     AddCtx, Component, Ctx, EventIdx, Expr, ExprIdx, Foldable, ParamIdx,
@@ -54,13 +54,21 @@ impl TimeIdx {
         time.event
     }
 
-    pub fn relevant_vars(
-        self,
-        ctx: &(impl Ctx<Time> + Ctx<Expr> + Ctx<Prop>),
-    ) -> Vec<ParamIdx> {
+    pub fn relevant_vars<C>(self, ctx: &C) -> Vec<ParamIdx>
+    where
+        C: Ctx<Time> + Ctx<Expr> + Ctx<Prop>,
+    {
         let time = ctx.get(self);
         time.offset.relevant_vars(ctx)
     }
+
+    pub fn valid<C>(&self, ctx: &C) -> bool
+    where
+        C: Ctx<Time> + Ctx<Expr> + Ctx<Prop> + MutCtx<Param>,
+    {
+        let time = ctx.get(*self);
+        time.offset.valid(ctx)
+    }
 }
 
 #[derive(PartialEq, Eq, Hash, Clone)]