diff --git a/axiom-profiler-GUI/src/configuration/data.rs b/axiom-profiler-GUI/src/configuration/data.rs
index ff7e02aa..bdd3e8d3 100644
--- a/axiom-profiler-GUI/src/configuration/data.rs
+++ b/axiom-profiler-GUI/src/configuration/data.rs
@@ -2,7 +2,7 @@ use fxhash::FxHashMap;
 use smt_log_parser::{
     display_with::{DisplayConfiguration, SymbolReplacement},
     formatter::TermDisplayContext,
-    NonMaxU32,
+    F64Ord, NonMaxU32,
 };
 
 use crate::screen::homepage::FileInfo;
@@ -47,6 +47,7 @@ impl ConfigurationProvider {
 pub struct Configuration {
     pub display: DisplayConfiguration,
     pub term_display: TermDisplayContextFiles,
+    pub avg_weighing: F64Ord,
 }
 impl Configuration {
     pub const fn default_display() -> DisplayConfiguration {
@@ -69,6 +70,7 @@ impl Default for Configuration {
         Self {
             display: Self::default_display(),
             term_display: TermDisplayContextFiles::default(),
+            avg_weighing: F64Ord(1.0),
         }
     }
 }
diff --git a/axiom-profiler-GUI/src/configuration/page.rs b/axiom-profiler-GUI/src/configuration/page.rs
index 1c1891c3..944fff79 100644
--- a/axiom-profiler-GUI/src/configuration/page.rs
+++ b/axiom-profiler-GUI/src/configuration/page.rs
@@ -1,6 +1,6 @@
 use std::rc::Rc;
 
-use smt_log_parser::{display_with::SymbolReplacement, NonMaxU32};
+use smt_log_parser::{display_with::SymbolReplacement, F64Ord, NonMaxU32};
 use wasm_bindgen::JsCast;
 use yew::{
     function_component, use_context, use_effect_with_deps, Callback, Event, Html, Properties,
@@ -129,6 +129,19 @@ pub fn Flags(props: &FlagsProps) -> Html {
     );
     use_effect_with_deps(move |deps| effect(deps), deps);
 
+    let (summary_weighing, effect, deps) = flag_widget!(
+        cfg,
+        default,
+        avg_weighing,
+        "Average weighing",
+        "When sorting by average, how much weight should be given to the total count. Currently only affects quantifier sorting on the summary screen. A weight of 0% means sorting exactly by the average, while N% means that anything with < N% of the total will be heavily down-ranked.", |
+        if F64Ord(0.0) => "0%",
+        if F64Ord(1.0) => "1%",
+        if F64Ord(10.0) => "10%",
+        if F64Ord(100.0) => "100%",
+    );
+    use_effect_with_deps(move |deps| effect(deps), deps);
+
     yew::html! {
         <div class="flags-page"><div class="flags-content">
             <h1>{"Configuration flags"}</h1>
@@ -136,6 +149,7 @@ pub fn Flags(props: &FlagsProps) -> Html {
             {debug}
             {replace_symbols}
             {ast_depth_limit}
+            {summary_weighing}
             <TermDisplayFlag cfg={cfg.clone()} file={props.file.clone()} />
         </div></div>
     }
diff --git a/axiom-profiler-GUI/src/screen/file/summary.rs b/axiom-profiler-GUI/src/screen/file/summary.rs
index 6570d731..3e5dc091 100644
--- a/axiom-profiler-GUI/src/screen/file/summary.rs
+++ b/axiom-profiler-GUI/src/screen/file/summary.rs
@@ -52,6 +52,7 @@ pub fn Summary(props: &SummaryProps) -> Html {
         analysis: props.analysis.clone(),
         term_display: term_display.clone(),
         config: cfg.config.display,
+        avg_weighing: cfg.config.avg_weighing.0,
     };
 
     let graph = props.analysis.clone().map(|analysis| {
@@ -68,6 +69,7 @@ pub fn Summary(props: &SummaryProps) -> Html {
             <Metrics ..inner.clone() />
             <MostQuants ..inner.clone() />
             <CostQuants ..inner.clone() />
+            <MultQuants ..inner.clone() />
         </DetailContainer><DetailContainer>
             <CostLemmas ..inner.clone() />
             <CostCdcl ..inner />
@@ -82,6 +84,7 @@ pub struct SummaryPropsInner {
     pub analysis: Option<RcAnalysis>,
     pub term_display: Rc<TermDisplayContext>,
     pub config: DisplayConfiguration,
+    pub avg_weighing: f64,
 }
 
 impl SummaryPropsInner {
@@ -138,13 +141,13 @@ pub fn MostQuants(props: &SummaryPropsInner) -> Html {
     let summary = &props.parser.summary;
     let colours = &props.parser.colour_map;
 
-    let quants = summary.log_info.quants_iter();
-    let quants = quants_ordered::<_, true>(&parser, colours, quants);
+    let quants = summary.log_info.quants_iter().map(|(q, c)| (q, (), c));
+    let quants = quants_ordered::<(), _, true>(&parser, colours, quants);
     let quants = quants
         .iter()
         .take(DISPLAY_TOP_N)
         .take_while(|(.., c)| *c > 0);
-    let quants = quants.map(|(q, hue, c)| {
+    let quants = quants.map(|(q, hue, (), c)| {
         let left = format_to_html(*c);
         let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
         (left, right)
@@ -158,24 +161,63 @@ pub fn MostQuants(props: &SummaryPropsInner) -> Html {
 #[function_component]
 pub fn CostQuants(props: &SummaryPropsInner) -> Html {
     props.analysis.as_ref().map(|analysis| {
+        let log_info = &props.parser.summary.log_info;
         let parser = props.parser.parser.borrow();
         let analysis = analysis.borrow();
         let colours = &props.parser.colour_map;
+        let offset = log_info.match_.quantifiers as f64 * props.avg_weighing / 100.;
 
-        let costs = analysis.quants.quants_costs().map(|(q, c)| (q, F64Ord(c)));
-        let costs = quants_ordered::<_, true>(&parser, colours, costs);
+        let costs = analysis.quants.quants_costs().map(|(q, c)| {
+            let qis = log_info.quant_insts(q);
+            if qis == 0 {
+                (q, 0.0, F64Ord(0.0))
+            } else {
+                (q, c / qis as f64, F64Ord(c / (qis as f64 + offset)))
+            }
+        });
+        let costs = quants_ordered::<_, _, true>(&parser, colours, costs);
         let costs = costs.iter().take(DISPLAY_TOP_N).take_while(|(.., c)| c.0 > 0.0);
-        let costs = costs.map(|(q, hue, c)| {
-            let left = format_to_html(c.0 as u64);
+        let costs = costs.map(|(q, hue, c, _)| {
+            let left = html!{{ format!("{c:.1}") }};
             let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
             (left, right)
         }).collect::<Vec<_>>();
-        html! {<Detail title="Most expensive quantifiers" hover="The quantifiers upon which the most instantiations depend.">
+        html! {<Detail title="Average cost" hover="The quantifiers upon which the most instantiations causally depend. See average weighing flag.">
             <TreeList elements={costs} />
         </Detail>}
     }).unwrap_or_default()
 }
 
+#[function_component]
+pub fn MultQuants(props: &SummaryPropsInner) -> Html {
+    props.analysis.as_ref().map(|analysis| {
+        let log_info = &props.parser.summary.log_info;
+        let parser = props.parser.parser.borrow();
+        let analysis = analysis.borrow();
+        let colours = &props.parser.colour_map;
+        let offset = log_info.match_.quantifiers as f64 * props.avg_weighing / 100.;
+
+        let mults = analysis.quants.quants_children().map(|(q, c)| {
+            let qis = log_info.quant_insts(q);
+            if qis == 0 {
+                (q, 0.0, F64Ord(0.0))
+            } else {
+                (q, c / qis as f64, F64Ord(c / (qis as f64 + offset)))
+            }
+        });
+        let mults = quants_ordered::<_, _, true>(&parser, colours, mults);
+        let mults = mults.iter().take(DISPLAY_TOP_N).take_while(|(.., c)| c.0 > 0.0);
+        let mults = mults.map(|(q, hue, c, _)| {
+            let left = html!{{ format!("{c:.1}") }};
+            let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
+            (left, right)
+        }).collect::<Vec<_>>();
+        html! {<Detail title="Average multiplicativity" hover="The quantifiers which the highest multiplicative factor, i.e. those that on average directly cause N other instantiations. See average weighing flag.">
+            <TreeList elements={mults} />
+        </Detail>}
+    }).unwrap_or_default()
+}
+
 #[function_component]
 pub fn CostLemmas(props: &SummaryPropsInner) -> Html {
     props.analysis.as_ref().map(|analysis| {
@@ -213,17 +255,17 @@ fn format_to_html<F: ToFormattedString>(f: F) -> Html {
     html! {{ f.to_formatted_string(&Locale::en) }}
 }
 
-fn quants_ordered<'a, T: Ord + Copy + Debug, const REVERSE: bool>(
+fn quants_ordered<'a, D, T: Ord + Copy + Debug, const REVERSE: bool>(
     parser: &'a Z3Parser,
     colour_map: &QuantIdxToColourMap,
-    quants: impl Iterator<Item = (QuantIdx, T)>,
-) -> Vec<(Cow<'a, str>, Option<f64>, T)> {
+    quants: impl Iterator<Item = (QuantIdx, D, T)>,
+) -> Vec<(Cow<'a, str>, Option<f64>, D, T)> {
     let mut quants = quants
-        .filter_map(|(q, c)| {
+        .filter_map(|(q, d, c)| {
             let name = parser[q].kind.name(&parser.strings)?;
             let hue = colour_map.get_rbg_hue(Some(q));
             // log::info!("{name}: {hue:?} | {c:?}");
-            Some((name, hue, c))
+            Some((name, hue, d, c))
         })
         .collect::<Vec<_>>();
     if REVERSE {
diff --git a/axiom-profiler-GUI/src/screen/inst_graph/filter/add_filter.rs b/axiom-profiler-GUI/src/screen/inst_graph/filter/add_filter.rs
index 7f15ac06..044206be 100644
--- a/axiom-profiler-GUI/src/screen/inst_graph/filter/add_filter.rs
+++ b/axiom-profiler-GUI/src/screen/inst_graph/filter/add_filter.rs
@@ -116,7 +116,7 @@ impl AddFilter<'_> {
             mk_filter(
                 &nodes,
                 |&(n, _, _)| {
-                    raw.neighbors_directed(n, Direction::Outgoing)
+                    raw.neighbors_directed(n, Direction::Outgoing, &self.graph.analysis.reach)
                         .count_hidden()
                         > 0
                 },
@@ -125,7 +125,7 @@ impl AddFilter<'_> {
             mk_filter(
                 &nodes,
                 |&(n, _, _)| {
-                    raw.neighbors_directed(n, Direction::Incoming)
+                    raw.neighbors_directed(n, Direction::Incoming, &self.graph.analysis.reach)
                         .count_hidden()
                         > 0
                 },
diff --git a/axiom-profiler-GUI/src/screen/inst_graph/filter/apply.rs b/axiom-profiler-GUI/src/screen/inst_graph/filter/apply.rs
index 5876f256..03c22e26 100644
--- a/axiom-profiler-GUI/src/screen/inst_graph/filter/apply.rs
+++ b/axiom-profiler-GUI/src/screen/inst_graph/filter/apply.rs
@@ -51,7 +51,10 @@ impl Filter {
             }
             MaxBranching(n) => graph.keep_first_n_children(n),
             ShowNeighbours(nidx, direction) => {
-                let nodes: Vec<_> = graph.raw.neighbors_directed(nidx, direction).collect();
+                let nodes: Vec<_> = graph
+                    .raw
+                    .neighbors_directed(nidx, direction, &graph.analysis.reach)
+                    .collect();
                 let modified = graph.raw.set_visibility_many(false, nodes.iter().copied());
                 select = Some(nodes);
                 modified
diff --git a/smt-log-parser/src/analysis/dependencies.rs b/smt-log-parser/src/analysis/dependencies.rs
index 1a813818..f0e5d714 100644
--- a/smt-log-parser/src/analysis/dependencies.rs
+++ b/smt-log-parser/src/analysis/dependencies.rs
@@ -17,6 +17,9 @@ pub struct QuantPatInfo {
     /// How much total cost did this quantifier + pattern accrue from individual
     /// instantiations.
     pub costs: f64,
+    /// How many other instantiations of other quantifiers is this quantifier
+    /// _directly_ responsible for.
+    pub children: f64,
     /// How many times does an instantiation of this quantifier depend on an
     /// instantiation of the other quantifier.
     pub direct_deps: Vec<DirectDep>,
@@ -49,6 +52,16 @@ impl QuantifierAnalysis {
             let ginst = &inst_graph.raw[data.iidx];
             qinfo.costs += ginst.cost;
 
+            for &child in ginst.children.insts.iter() {
+                let cq = parser.get_inst(child).match_.kind.quant_idx();
+                if cq.is_some_and(|q| q == qpat.quant) {
+                    // Skip self references.
+                    continue;
+                }
+                let parents = inst_graph.raw[child].parents.insts.len() as f64;
+                qinfo.children += 1.0 / parents;
+            }
+
             let pat = parser.get_pattern(qpat);
             let subpats = pat.map(|p| parser[p].child_ids.len()).unwrap_or_default();
             for (i, blame) in data.match_.pattern_matches().enumerate() {
@@ -97,6 +110,13 @@ impl QuantifierAnalysis {
             .map(|(quant, data)| (quant, data.iter_enumerated().map(|(_, d)| d.costs).sum()))
     }
 
+    pub fn quants_children(&self) -> impl Iterator<Item = (QuantIdx, f64)> + '_ {
+        self.0
+             .0
+            .iter_enumerated()
+            .map(|(quant, data)| (quant, data.iter_enumerated().map(|(_, d)| d.children).sum()))
+    }
+
     pub fn calculate_transitive(&self, mut steps: Option<u32>) -> TransQuantAnalaysis {
         let mut initial: TiVec<QuantIdx, _> =
             (0..self.0 .0.len()).map(|_| FxHashSet::default()).collect();
diff --git a/smt-log-parser/src/analysis/graph/analysis/mod.rs b/smt-log-parser/src/analysis/graph/analysis/mod.rs
index 4453ff24..bd1a8852 100644
--- a/smt-log-parser/src/analysis/graph/analysis/mod.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/mod.rs
@@ -14,13 +14,14 @@ use mem_dbg::{MemDbg, MemSize};
 
 use matching_loop::MlData;
 
-use crate::{F64Ord, Result, Z3Parser};
+use crate::{F64Ord, Result, TiVec, Z3Parser};
 
 use self::{
     cost::{DefaultCost, ProofCost},
     depth::DefaultDepth,
     next_nodes::NextInstsInit,
     proof::ProofInitialiser,
+    reconnect::{BwdReachableAnalysis, ReachNonDisabled},
 };
 
 use super::{raw::RawInstGraph, InstGraph, RawNodeIndex};
@@ -28,6 +29,7 @@ use super::{raw::RawInstGraph, InstGraph, RawNodeIndex};
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug, Default)]
 pub struct Analysis {
+    pub reach: TiVec<RawNodeIndex, ReachNonDisabled>,
     // Highest to lowest
     pub cost: OrderingAnalysis,
     // Most to least
@@ -89,6 +91,7 @@ impl Analysis {
         // Alloc `fwd_depth_min` vector
         let fwd_depth_min = cost.duplicate()?;
         Ok(Self {
+            reach: Default::default(),
             cost,
             children,
             fwd_depth_min,
@@ -107,6 +110,9 @@ impl InstGraph {
     }
 
     pub fn initialise_default(&mut self, parser: &Z3Parser) {
+        let mut reach = BwdReachableAnalysis::<ReachNonDisabled>::default();
+        self.analysis.reach = self.topo_analysis(&mut reach);
+
         self.initialise_transfer(DefaultCost, parser);
         self.initialise_transfer(ProofCost, parser);
         self.initialise_collect(DefaultDepth::<true>, parser);
diff --git a/smt-log-parser/src/analysis/graph/analysis/reconnect.rs b/smt-log-parser/src/analysis/graph/analysis/reconnect.rs
index 28561e83..6a76f64a 100644
--- a/smt-log-parser/src/analysis/graph/analysis/reconnect.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/reconnect.rs
@@ -1,5 +1,8 @@
 use std::collections::hash_map::Entry;
 
+#[cfg(feature = "mem_dbg")]
+use mem_dbg::{MemDbg, MemSize};
+
 use fxhash::FxHashSet;
 
 use crate::{
@@ -9,10 +12,52 @@ use crate::{
 
 use super::run::TopoAnalysis;
 
-pub struct BwdReachableVisAnalysis;
+pub trait ReachKind: Copy + core::fmt::Debug + From<bool> + Into<bool> {
+    fn current(node: &Node) -> Self;
+    fn value(self) -> bool {
+        self.into()
+    }
+}
+
+macro_rules! reach_kind {
+    ($name:ident($node:ident => $e:expr)) => {
+        #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
+        #[cfg_attr(feature = "mem_dbg", copy_type)]
+        #[derive(Debug, Clone, Copy)]
+        pub struct $name(bool);
+        impl ReachKind for $name {
+            fn current($node: &Node) -> Self {
+                Self($e)
+            }
+        }
+        impl From<bool> for $name {
+            fn from(b: bool) -> Self {
+                Self(b)
+            }
+        }
+        impl From<$name> for bool {
+            fn from(b: $name) -> bool {
+                b.0
+            }
+        }
+    };
+}
+
+reach_kind!(ReachVisible(node => node.visible()));
+reach_kind!(ReachNonDisabled(node => !node.disabled()));
 
-impl TopoAnalysis<false, false> for BwdReachableVisAnalysis {
-    type Value = bool;
+/// If `VIS` is true, then it checks if a visible node is reachable from this
+/// one, otherwise it checks if any non-disabled node is reachable.
+#[derive(Clone, Copy)]
+pub struct BwdReachableAnalysis<Kind: ReachKind>(core::marker::PhantomData<Kind>);
+impl<Kind: ReachKind> Default for BwdReachableAnalysis<Kind> {
+    fn default() -> Self {
+        Self(Default::default())
+    }
+}
+
+impl<Kind: ReachKind> TopoAnalysis<false, false> for BwdReachableAnalysis<Kind> {
+    type Value = Kind;
 
     fn collect<'a, 'n, T: Iterator<Item = (RawNodeIndex, &'n Self::Value)>>(
         &mut self,
@@ -24,11 +69,9 @@ impl TopoAnalysis<false, false> for BwdReachableVisAnalysis {
     where
         Self::Value: 'n,
     {
-        if node.visible() {
-            true
-        } else {
-            from_all().any(|(_, &b)| b)
-        }
+        let curr = Kind::current(node).value();
+        let reach = curr || from_all().any(|(_, &b)| b.value());
+        reach.into()
     }
 }
 
@@ -42,7 +85,7 @@ impl TopoAnalysis<false, false> for BwdReachableVisAnalysis {
 ///
 /// The `to` is implicit in the index which we used to reach the
 /// `TopoAnalysis::Value`.
-pub struct ReconnectAnalysis(pub TiVec<RawNodeIndex, bool>);
+pub struct ReconnectAnalysis(pub TiVec<RawNodeIndex, ReachVisible>);
 
 #[derive(Debug, Default)]
 pub struct ReconnectData {
@@ -164,7 +207,7 @@ impl TopoAnalysis<true, false> for ReconnectAnalysis {
         Self::Value: 'n,
     {
         let mut data = Self::Value::default();
-        if !self.0[cidx] {
+        if !self.0[cidx].value() {
             return data;
         }
 
diff --git a/smt-log-parser/src/analysis/graph/analysis/run.rs b/smt-log-parser/src/analysis/graph/analysis/run.rs
index 4cc26a33..07d3b78b 100644
--- a/smt-log-parser/src/analysis/graph/analysis/run.rs
+++ b/smt-log-parser/src/analysis/graph/analysis/run.rs
@@ -10,6 +10,8 @@ use crate::{
     TiVec, Z3Parser,
 };
 
+use super::reconnect::ReachNonDisabled;
+
 // FIXME: `ID` makes the implementations unique, but is not a great solution.
 /// FORWARD: Do a forward or reverse topological walk?
 pub trait Initialiser<const FORWARD: bool, const ID: u8> {
@@ -75,9 +77,10 @@ impl RawInstGraph {
         &self,
         curr: RawNodeIndex,
         dir: Direction,
+        reach: &TiVec<RawNodeIndex, ReachNonDisabled>,
     ) -> impl Iterator<Item = RawNodeIndex> + '_ {
         if SKIP_DISABLED {
-            either::Either::Left(self.neighbors_directed(curr, dir))
+            either::Either::Left(self.neighbors_directed(curr, dir, reach))
         } else {
             either::Either::Right(self.graph.neighbors_directed(curr.0, dir).map(RawNodeIndex))
         }
@@ -119,7 +122,7 @@ impl InstGraph {
                 } else {
                     let from_all = || {
                         self.raw
-                            .neighbors_directed_::<SKIP_DISABLED>(curr, dir)
+                            .neighbors_directed_::<SKIP_DISABLED>(curr, dir, &self.analysis.reach)
                             .map(|i| {
                                 let data = &data[i];
                                 // Safety: The data is initialised as the graph is a DAG
@@ -175,7 +178,11 @@ impl InstGraph {
             let for_each = |idx: RawNodeIndex| {
                 let from_all = || {
                     self.raw
-                        .neighbors_directed_::<SKIP_DISABLED>(idx, I::direction())
+                        .neighbors_directed_::<SKIP_DISABLED>(
+                            idx,
+                            I::direction(),
+                            &self.analysis.reach,
+                        )
                         .map(|i| &self.raw[i])
                 };
                 let value = initialiser.collect(&self.raw.graph[idx.0], from_all);
@@ -209,11 +216,14 @@ impl InstGraph {
             let for_each = |idx: RawNodeIndex| {
                 let incoming: Vec<_> = self
                     .raw
-                    .neighbors_directed(idx, I::direction())
+                    .neighbors_directed(idx, I::direction(), &self.analysis.reach)
                     .map(|i| initialiser.observe(&self.raw[i], parser))
                     .collect();
                 let mut i = 0;
-                let mut neighbors = self.raw.neighbors_directed(idx, I::direction()).detach();
+                let mut neighbors = self
+                    .raw
+                    .neighbors_directed(idx, I::direction(), &self.analysis.reach)
+                    .detach();
                 while let Some(neighbor) = neighbors.next(&self.raw) {
                     let transfer = initialiser.transfer(&self.raw.graph[idx.0], idx, i, &incoming);
                     initialiser.add(&mut self.raw[neighbor], transfer);
diff --git a/smt-log-parser/src/analysis/graph/raw.rs b/smt-log-parser/src/analysis/graph/raw.rs
index 6f4ff49f..3d643922 100644
--- a/smt-log-parser/src/analysis/graph/raw.rs
+++ b/smt-log-parser/src/analysis/graph/raw.rs
@@ -18,9 +18,11 @@ use crate::{
         CdclIdx, ENodeBlame, ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, GraphIdx, InstIdx,
         ProofIdx, StackIdx, TransitiveExplSegmentKind,
     },
-    DiGraph, FxHashMap, FxHashSet, NonMaxU32, Result, Z3Parser,
+    DiGraph, FxHashMap, FxHashSet, NonMaxU32, Result, TiVec, Z3Parser,
 };
 
+use super::analysis::reconnect::{ReachKind, ReachNonDisabled};
+
 graph_idx!(raw_idx, RawNodeIndex, RawEdgeIndex, RawIx);
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
@@ -251,20 +253,34 @@ impl RawInstGraph {
     /// Similar to `self.graph.neighbors` but will walk through disabled nodes.
     ///
     /// Note: Iterating the neighbors is **not** a O(1) operation.
-    pub fn neighbors(&self, node: RawNodeIndex) -> Neighbors<'_> {
-        self.neighbors_directed(node, Direction::Outgoing)
+    pub fn neighbors(
+        &self,
+        node: RawNodeIndex,
+        reach: &TiVec<RawNodeIndex, ReachNonDisabled>,
+    ) -> Neighbors<'_> {
+        self.neighbors_directed(node, Direction::Outgoing, reach)
     }
+
     /// Similar to `self.graph.neighbors_directed` but will walk through
     /// disabled nodes.
     ///
     /// Note: Iterating the neighbors is **not** a O(1) operation.
-    pub fn neighbors_directed(&self, node: RawNodeIndex, dir: Direction) -> Neighbors<'_> {
+    pub fn neighbors_directed(
+        &self,
+        node: RawNodeIndex,
+        dir: Direction,
+        reach: &TiVec<RawNodeIndex, ReachNonDisabled>,
+    ) -> Neighbors<'_> {
         let direct = self.graph.neighbors_directed(node.0, dir).detach();
-        let walk = WalkNeighbors {
-            dir,
-            visited: FxHashSet::default(),
-            stack: Vec::new(),
-            direct,
+        let walk = if reach.get(node).is_some_and(|v| !v.value()) {
+            WalkNeighbors::None
+        } else {
+            WalkNeighbors::Some {
+                dir,
+                visited: FxHashSet::default(),
+                stack: Vec::new(),
+                direct,
+            }
         };
         Neighbors { raw: self, walk }
     }
@@ -706,15 +722,27 @@ impl Iterator for Neighbors<'_> {
 }
 
 #[derive(Clone)]
-pub struct WalkNeighbors {
-    pub dir: Direction,
-    pub visited: FxHashSet<RawNodeIndex>,
-    pub stack: Vec<RawNodeIndex>,
-    pub direct: petgraph::graph::WalkNeighbors<RawIx>,
+pub enum WalkNeighbors {
+    None,
+    Some {
+        dir: Direction,
+        visited: FxHashSet<RawNodeIndex>,
+        stack: Vec<RawNodeIndex>,
+        direct: petgraph::graph::WalkNeighbors<RawIx>,
+    },
 }
 
 impl WalkNeighbors {
     pub fn next(&mut self, raw: &RawInstGraph) -> Option<RawNodeIndex> {
+        let WalkNeighbors::Some {
+            dir,
+            visited,
+            stack,
+            direct,
+        } = self
+        else {
+            return None;
+        };
         // TODO: decide if we want to prevent direct neighbors from being
         // visited multiple times if there are multiple direct edges.
         loop {
@@ -727,22 +755,17 @@ impl WalkNeighbors {
             //     }
             // }
             // let idx = idx.or_else(|| self.stack.pop())?;
-            let idx = self
-                .direct
+            let idx = direct
                 .next(&raw.graph)
                 .map(|(_, n)| RawNodeIndex(n))
-                .or_else(|| self.stack.pop())?;
+                .or_else(|| stack.pop())?;
             let node = &raw[idx];
             if !node.disabled() {
                 return Some(idx);
             }
-            for n in raw
-                .graph
-                .neighbors_directed(idx.0, self.dir)
-                .map(RawNodeIndex)
-            {
-                if self.visited.insert(n) {
-                    self.stack.push(n);
+            for n in raw.graph.neighbors_directed(idx.0, *dir).map(RawNodeIndex) {
+                if visited.insert(n) {
+                    stack.push(n);
                 }
             }
         }
diff --git a/smt-log-parser/src/analysis/graph/visible.rs b/smt-log-parser/src/analysis/graph/visible.rs
index 916c8094..b9271cd9 100644
--- a/smt-log-parser/src/analysis/graph/visible.rs
+++ b/smt-log-parser/src/analysis/graph/visible.rs
@@ -14,7 +14,7 @@ use crate::{
 };
 
 use super::{
-    analysis::reconnect::{BwdReachableVisAnalysis, ReconnectAnalysis},
+    analysis::reconnect::{BwdReachableAnalysis, ReachVisible, ReconnectAnalysis},
     raw::{EdgeKind, NodeKind},
     InstGraph, RawEdgeIndex, RawNodeIndex,
 };
@@ -30,7 +30,8 @@ pub struct VisibleInstGraph {
 
 impl InstGraph {
     pub fn to_visible(&self) -> VisibleInstGraph {
-        let bwd_vis_reachable = self.topo_analysis(&mut BwdReachableVisAnalysis);
+        let mut reach = BwdReachableAnalysis::<ReachVisible>::default();
+        let bwd_vis_reachable = self.topo_analysis(&mut reach);
         let mut reconnect = self.topo_analysis(&mut ReconnectAnalysis(bwd_vis_reachable));
         let (mut nodes, mut edges) = (0, 0);
         for (idx, data) in reconnect.iter_mut_enumerated() {
@@ -49,8 +50,14 @@ impl InstGraph {
             if !self.raw[idx].visible() {
                 continue;
             }
-            let hidden_parents = self.raw.neighbors_directed(idx, Incoming).count_hidden();
-            let hidden_children = self.raw.neighbors_directed(idx, Outgoing).count_hidden();
+            let hidden_parents = self
+                .raw
+                .neighbors_directed(idx, Incoming, &self.analysis.reach)
+                .count_hidden();
+            let hidden_children = self
+                .raw
+                .neighbors_directed(idx, Outgoing, &self.analysis.reach)
+                .count_hidden();
             let v_node = VisibleNode {
                 idx,
                 hidden_parents: hidden_parents as u32,
diff --git a/smt-log-parser/src/analysis/misc.rs b/smt-log-parser/src/analysis/misc.rs
index b3f9eb4d..0c216cf8 100644
--- a/smt-log-parser/src/analysis/misc.rs
+++ b/smt-log-parser/src/analysis/misc.rs
@@ -105,4 +105,11 @@ impl LogInfo {
             .iter_enumerated()
             .map(|(i, count)| (i, count.iter_enumerated().map(|(_, c)| c).sum()))
     }
+
+    pub fn quant_insts(&self, qidx: QuantIdx) -> usize {
+        self.quants.0 .0[qidx]
+            .iter_enumerated()
+            .map(|(_, c)| *c)
+            .sum()
+    }
 }
diff --git a/smt-log-parser/src/util.rs b/smt-log-parser/src/util.rs
index a42c7523..8010c47f 100644
--- a/smt-log-parser/src/util.rs
+++ b/smt-log-parser/src/util.rs
@@ -1,5 +1,11 @@
-#[derive(Debug, Clone, Copy, PartialEq)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+#[derive(Debug, Clone, Copy)]
 pub struct F64Ord(pub f64);
+impl std::cmp::PartialEq for F64Ord {
+    fn eq(&self, other: &Self) -> bool {
+        self.0.total_cmp(&other.0).is_eq()
+    }
+}
 impl std::cmp::Eq for F64Ord {}
 impl std::cmp::PartialOrd for F64Ord {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {