diff --git a/act/back_end/core.py b/act/back_end/core.py
index 7aa7f4b68..1df58820b 100644
--- a/act/back_end/core.py
+++ b/act/back_end/core.py
@@ -60,27 +60,8 @@ def get_bounds_for_var(self, fact: 'Fact', var_id: int, is_output: bool = True)
         
         return lb, ub
     
-    def get_all_var_bounds(self, fact: 'Fact', is_output: bool = True) -> Dict[int, Tuple[float, float]]:
-        """Get dict of {var_id: (lb, ub)} for all variables. Use is_output=True for out_vars, False for in_vars."""
-        var_list = self.out_vars if is_output else self.in_vars
-        
-        bounds_dict = {}
-        for var_id in var_list:
-            bounds_dict[var_id] = self.get_bounds_for_var(fact, var_id, is_output)
-        
-        return bounds_dict
     
-    def get_input_shape(self) -> Optional[Tuple[int, ...]]:
-        """Get input shape from params, or None if not stored."""
-        if self.kind == "INPUT":
-            return self.params.get("shape")
-        return self.params.get("input_shape")
     
-    def get_output_shape(self) -> Optional[Tuple[int, ...]]:
-        """Get output shape from params, or None if not stored."""
-        if self.kind == "INPUT":
-            return self.params.get("shape")
-        return self.params.get("output_shape")
     
     def get_tensor(self, key: str, default: Optional[torch.Tensor] = None) -> Optional[torch.Tensor]:
         """Get tensor parameter. Returns default if missing or not a tensor."""
@@ -107,13 +88,7 @@ def is_tensor(self, key: str) -> bool:
         """Check if parameter is a tensor."""
         return isinstance(self.params.get(key), torch.Tensor)
     
-    def get_num_input_vars(self) -> int:
-        """Get number of input variables (flattened dimension)."""
-        return len(self.in_vars)
     
-    def get_num_output_vars(self) -> int:
-        """Get number of output variables (flattened dimension)."""
-        return len(self.out_vars)
 
 @dataclass
 class Net:
@@ -132,10 +107,6 @@ def __post_init__(self):
         validate_wrapper_graph(self.layers)
 
     # helpers
-    def last_validation(self) -> Optional[Layer]:
-        for L in reversed(self.layers):
-            if L.is_validation(): return L
-        return None
 
     def assert_last_is_validation(self) -> None:
         if not self.layers or not self.layers[-1].is_validation():
@@ -158,12 +129,6 @@ def get_all_predecessor_bounds(self, layer_id: int, after: Dict[int, 'Fact'],
         return [self.get_predecessor_bounds(layer_id, after, before, i) 
                 for i in range(len(self.preds[layer_id]))]
     
-    def get_layer_shape(self, layer_id: int, facts: Dict[int, 'Fact'], 
-                        is_output: bool = True) -> Tuple[int, ...]:
-        """Get shape from bounds tensor in facts dict. Use is_output=True for output shape, False for input."""
-        if layer_id not in facts:
-            raise KeyError(f"Layer {layer_id} not found in facts dictionary")
-        return facts[layer_id].bounds.lb.shape
         
         
 def topological_sort(net: Net, reverse: bool = False) -> List[int]:
@@ -251,38 +216,17 @@ def add_box(self, layer_id: int, var_ids: List[int], B: Bounds):
                           "lb": B.lb.detach().reshape(-1).clone(),
                           "ub": B.ub.detach().reshape(-1).clone()}))
         
-    def add_op(self, tag: str, var_ids: List[int], **meta):
-        """
-        Generic operator constraint container.
-        - tag: e.g. "dense:12", "relu:5"
-        - var_ids: ordered exactly as exporter expects
-        - meta: payload used by cons_exportor.py
-        """
-        op = tag.split(":", 1)[0]
-        if op and not self._is_op_supported_by_exporter(op):
-            raise ValueError(
-                f"Unknown op tag '{op}' (tag='{tag}'). "
-                "Update act/back_end/layer_schema.py SUPPORTED_EXPORT_OPS "
-                "and exporter handling if intentional."
-            )
-        m = {"tag": tag}
-        m.update(meta)
-        self.replace(Con("INEQ", tuple(var_ids), m))
     
     @staticmethod
     def _is_op_supported_by_exporter(op: str) -> bool:
-        """
-        Best-effort early validation against exporter registry.
-        Falls back to allow if exporter cannot be imported.
-        """
-        try:
-            mod = importlib.import_module("act.back_end.layer_util")
-            fn = getattr(mod, "is_supported_op", None)
-            if fn is None:
-                return True
-            return bool(fn(op))
-        except Exception:
-            return True
+        """Validate an operator against the exporter registry."""
+        mod = importlib.import_module("act.back_end.layer_util")
+        fn = getattr(mod, "is_supported_op", None)
+        if fn is None:
+            raise RuntimeError(
+                f"Exporter capability function is_supported_op is missing while checking {op!r}"
+            )
+        return bool(fn(op))
 
     def __iter__(self):
         """Iterate over constraints (Con objects). Makes ConSet iterable."""
diff --git a/act/back_end/hybridz_tf/hybridz_tf.py b/act/back_end/hybridz_tf/hybridz_tf.py
index afad49158..bdd706316 100644
--- a/act/back_end/hybridz_tf/hybridz_tf.py
+++ b/act/back_end/hybridz_tf/hybridz_tf.py
@@ -388,20 +388,17 @@ def _sparse_fact(fact: Fact, hz: SparseHZono) -> Fact:
 
     def _seed_sparse_cache(self, L: Layer, input_bounds: Bounds) -> None:
         k = L.kind.upper()
-        try:
-            if k in ("INPUT", "INPUT_SPEC"):
+        if k in ("INPUT", "INPUT_SPEC"):
+            self._sparse_hz_cache[L.id] = self._sparse_from_bounds(input_bounds)
+            self._sparse_drop_reasons.pop(L.id, None)
+        elif k != "ASSERT":
+            preds = self._net.preds.get(L.id, [])
+            if preds and preds[0] in self._sparse_hz_cache:
+                self._sparse_hz_cache[L.id] = self._sparse_hz_cache[preds[0]]
+                self._sparse_drop_reasons.pop(L.id, None)
+            elif not preds:
                 self._sparse_hz_cache[L.id] = self._sparse_from_bounds(input_bounds)
                 self._sparse_drop_reasons.pop(L.id, None)
-            elif k != "ASSERT":
-                preds = self._net.preds.get(L.id, [])
-                if preds and preds[0] in self._sparse_hz_cache:
-                    self._sparse_hz_cache[L.id] = self._sparse_hz_cache[preds[0]]
-                    self._sparse_drop_reasons.pop(L.id, None)
-                elif not preds:
-                    self._sparse_hz_cache[L.id] = self._sparse_from_bounds(input_bounds)
-                    self._sparse_drop_reasons.pop(L.id, None)
-        except Exception as exc:
-            self._drop_sparse_hz(L.id, f"sparse_seed_failed:{type(exc).__name__}")
 
     def _drop_sparse_hz(self, layer_id: int, reason: str) -> None:
         lid = int(layer_id)
@@ -423,24 +420,21 @@ def _propagate_sparse_hz(self, L: Layer, input_bounds: Bounds, result: Fact) ->
         if self._sparse_exceeds_limit(hz, result.bounds.lb.numel()):
             self._drop_sparse_hz(L.id, f"sparse_size_limit:{k}")
             return result
-        try:
-            for apply_sparse in (
-                hz_mlp.sparse_hz_apply_layer,
-                hz_cnn.sparse_hz_apply_layer,
-                hz_transformer.sparse_hz_apply_layer,
-            ):
-                handled, out, drop_reason = apply_sparse(L, hz, input_bounds, result, self)
-                if not handled:
-                    continue
-                if out is None:
-                    self._drop_sparse_hz(L.id, drop_reason or f"unsupported_sparse_op:{k}")
-                    return result
-                self._sparse_hz_cache[L.id] = out
-                self._sparse_drop_reasons.pop(L.id, None)
-                return self._sparse_fact(result, out)
-            self._drop_sparse_hz(L.id, f"unsupported_sparse_op:{k}")
-        except Exception as exc:
-            self._drop_sparse_hz(L.id, f"sparse_op_failed:{k}:{type(exc).__name__}")
+        for apply_sparse in (
+            hz_mlp.sparse_hz_apply_layer,
+            hz_cnn.sparse_hz_apply_layer,
+            hz_transformer.sparse_hz_apply_layer,
+        ):
+            handled, out, drop_reason = apply_sparse(L, hz, input_bounds, result, self)
+            if not handled:
+                continue
+            if out is None:
+                self._drop_sparse_hz(L.id, drop_reason or f"unsupported_sparse_op:{k}")
+                return result
+            self._sparse_hz_cache[L.id] = out
+            self._sparse_drop_reasons.pop(L.id, None)
+            return self._sparse_fact(result, out)
+        self._drop_sparse_hz(L.id, f"unsupported_sparse_op:{k}")
         return result
 
     def apply(
diff --git a/act/back_end/hybridz_tf/tf_mlp.py b/act/back_end/hybridz_tf/tf_mlp.py
index 213acf56f..e697d4dc4 100644
--- a/act/back_end/hybridz_tf/tf_mlp.py
+++ b/act/back_end/hybridz_tf/tf_mlp.py
@@ -167,6 +167,7 @@ def _matmul_term_rows(L, batch: int):
     y_shape = tuple(int(d) for d in L.params["y_shape"])
     if len(x_shape) < 2 or len(y_shape) < 2 or x_shape[-1] != y_shape[-2]:
         return None
+    rows = None
     try:
         batch_shape = np.broadcast_shapes(x_shape[:-2], y_shape[:-2])
         m, reduction, n = x_shape[-2], x_shape[-1], y_shape[-1]
@@ -185,8 +186,13 @@ def _matmul_term_rows(L, batch: int):
             np.swapaxes(y_local, -2, -1)[..., None, :, :],
             (*batch_shape, m, n, reduction),
         ).reshape(-1, reduction)
+        rows = (x_terms, y_terms, reduction)
     except (ValueError, TypeError):
+        # Non-broadcastable MATMUL metadata is not applicable to sparse lifting.
+        rows = None
+    if rows is None:
         return None
+    x_terms, y_terms, reduction = rows
     x_size, y_size = _prod(x_shape), _prod(y_shape)
     offsets = np.arange(int(batch), dtype=np.int64)[:, None, None]
     return (
@@ -1169,12 +1175,14 @@ def _row_indices_expand(L, n: int):
     if per == 0 or int(n) % per != 0:
         return None
     batch = int(n) // per
-    try:
-        return torch.arange(int(n)).view(batch, *in_shape).broadcast_to(
-            batch, *out_shape
-        ).reshape(-1)
-    except RuntimeError:
+    source_shape = (batch, *in_shape)
+    target_shape = (batch, *out_shape)
+    if len(source_shape) > len(target_shape) or any(
+        source not in (1, target)
+        for source, target in zip(reversed(source_shape), reversed(target_shape))
+    ):
         return None
+    return torch.arange(int(n)).view(source_shape).broadcast_to(target_shape).reshape(-1)
 
 
 def _row_indices_reduce(L, n_in: int, n_out: int, axes_key: str, keepdims_key: str):
diff --git a/act/back_end/hybridz_tf/tf_transformer.py b/act/back_end/hybridz_tf/tf_transformer.py
index 977cd8b39..2fd4d3ba9 100644
--- a/act/back_end/hybridz_tf/tf_transformer.py
+++ b/act/back_end/hybridz_tf/tf_transformer.py
@@ -157,13 +157,16 @@ def _attention_score_differences(L, bounds: Bounds, rowsize: int, tf):
             continue
         if kind in {"SCALE", "BIAS"}:
             key = "a" if kind == "SCALE" else "c"
-            try:
-                value = (
-                    _broadcast_flat(score_layer.params[key], n_scores)
-                    .detach().cpu().double().numpy()
-                )
-            except ValueError:
+            raw_value = score_layer.params[key]
+            value_count = int(raw_value.numel())
+            if value_count == 0 or (
+                value_count not in (1, n_scores) and n_scores % value_count != 0
+            ):
                 return None
+            value = (
+                _broadcast_flat(raw_value, n_scores)
+                .detach().cpu().double().numpy()
+            )
             if kind == "SCALE":
                 scale *= value
             else:
diff --git a/act/back_end/layer_util.py b/act/back_end/layer_util.py
index 425d0e106..bf5eda83c 100644
--- a/act/back_end/layer_util.py
+++ b/act/back_end/layer_util.py
@@ -44,11 +44,8 @@
         # Will import at runtime when needed to avoid circular import
         pass
 
-try:
-    import torch
-    Tensor = torch.Tensor
-except Exception:  # typing only
-    Tensor = "torch.Tensor"  # type: ignore
+import torch
+Tensor = torch.Tensor
 
 # ------------------------------
 # Strict validation & helpers
@@ -250,54 +247,49 @@ def create_layer(id: int, kind: str, params: Dict[str, Any],
 # Tiny example (run file)
 # ---------------------
 if __name__ == "__main__":
-    try:
-        import torch  # type: ignore
-        import sys
-        import os
-        # Add parent directory to path for absolute imports
-        from act.util.path_config import get_project_root
-        project_root = get_project_root()
-        sys.path.insert(0, project_root)
+    import sys
+    # Add parent directory to path for absolute imports
+    from act.util.path_config import get_project_root
+    project_root = get_project_root()
+    sys.path.insert(0, project_root)
         
-        from act.back_end.core import Layer
-        from act.back_end.layer_schema import LayerKind
-        from typing import List
-        layers: List[Layer] = []
+    from act.back_end.core import Layer
+    from act.back_end.layer_schema import LayerKind
+    from typing import List
+    layers: List[Layer] = []
 
-        # INPUT
-        layers.append(create_layer(
+    # INPUT
+    layers.append(create_layer(
             id=0, kind=LayerKind.INPUT.value,
             params={},
             in_vars=[0], out_vars=[0],
-        ))
-        # SPEC (directly after INPUT - no adapters)
-        lb_tensor = torch.full((1,3,32,32), -1.0)
-        ub_tensor = torch.full((1,3,32,32), 1.0)
-        layers.append(create_layer(
+    ))
+    # SPEC (directly after INPUT - no adapters)
+    lb_tensor = torch.full((1,3,32,32), -1.0)
+    ub_tensor = torch.full((1,3,32,32), 1.0)
+    layers.append(create_layer(
             id=1, kind=LayerKind.INPUT_SPEC.value,
             params={"kind": InKind.BOX, "lb": lb_tensor, "ub": ub_tensor},
             in_vars=[0], out_vars=[0],
-        ))
-        # Model toy
-        layers.append(create_layer(
+    ))
+    # Model toy
+    layers.append(create_layer(
             id=2, kind=LayerKind.FLATTEN.value,
             params={},
             in_vars=[0], out_vars=[1],
-        ))
-        W, b = torch.randn(10, 3072), torch.randn(10)
-        layers.append(create_layer(
+    ))
+    W, b = torch.randn(10, 3072), torch.randn(10)
+    layers.append(create_layer(
             id=3, kind=LayerKind.DENSE.value,
             params={"W": W, "b": b},
             in_vars=[1], out_vars=[2],
-        ))
-        layers.append(create_layer(
+    ))
+    layers.append(create_layer(
             id=4, kind=LayerKind.ASSERT.value,
             params={},
             in_vars=[2], out_vars=[2],
-        ))
+    ))
 
-        validate_graph(layers)
-        validate_wrapper_graph(layers)
-        print("OK — wrapper model passes with", len(layers), "layers.")
-    except Exception as e:
-        print("Example failed:\n", e)
\ No newline at end of file
+    validate_graph(layers)
+    validate_wrapper_graph(layers)
+    print("OK — wrapper model passes with", len(layers), "layers.")
diff --git a/act/back_end/net_factory.py b/act/back_end/net_factory.py
index 38ce0dbec..b9e0c11e0 100644
--- a/act/back_end/net_factory.py
+++ b/act/back_end/net_factory.py
@@ -296,15 +296,6 @@ def append_binary_op(layers, *, op_kind: str, x_idx: int, y_idx: int) -> None:
     )
 
 
-def append_concat(layers, *, input_indices: List[int], concat_dim: int = 0) -> None:
-    _append_layer(
-        layers,
-        LayerKind.CONCAT.value,
-        params={"concat_dim": concat_dim},
-        preds=input_indices,
-    )
-
-
 def append_flatten(layers) -> None:
     _append_layer(layers, LayerKind.FLATTEN.value, params={"start_dim": 1})
 
@@ -1186,11 +1177,7 @@ def __init__(
         self.total_generated = 0
 
     def _compute_allowed_layers(self, tf_targets, mode):
-        try:
-            return _get_allowed_layers(tf_targets, mode)
-        except Exception as e:
-            logger.warning("TF capabilities unavailable: %s. Using defaults.", e)
-            return frozenset(_DEFAULT_COVERAGE_LAYERS)
+        return _get_allowed_layers(tf_targets, mode)
 
     def _init_coverage(self):
         skip = {
diff --git a/act/back_end/serialization/serialization.py b/act/back_end/serialization/serialization.py
index d1d797fdf..2f28c0c11 100644
--- a/act/back_end/serialization/serialization.py
+++ b/act/back_end/serialization/serialization.py
@@ -142,34 +142,14 @@ def deserialize_layer(layer_dict: Dict[str, Any], target_device: Optional[str] =
                 # This is a regular value
                 cache_decoded[name] = value
         
-        try:
-            layer = Layer(
-                id=layer_dict["id"],
-                kind=layer_dict["kind"],
-                params=params_decoded,
-                in_vars=layer_dict["in_vars"],
-                out_vars=layer_dict["out_vars"],
-                cache=cache_decoded
-            )
-        except ValueError as e:
-            # If core validation fails during deserialization, create the Layer
-            # without validation for template/example usage
-            if "schema violation" in str(e):
-                print(f"⚠️  Creating example/template layer {layer_dict['kind']}(id={layer_dict['id']}) without validation")
-                
-                # Create Layer without validation
-                layer = object.__new__(Layer)
-                layer.id = layer_dict["id"]
-                layer.kind = layer_dict["kind"]
-                layer.params = params_decoded
-                layer.in_vars = layer_dict["in_vars"]
-                layer.out_vars = layer_dict["out_vars"]
-                layer.cache = cache_decoded
-            else:
-                # Re-raise for other types of errors
-                raise
-
-        return layer
+        return Layer(
+            id=layer_dict["id"],
+            kind=layer_dict["kind"],
+            params=params_decoded,
+            in_vars=layer_dict["in_vars"],
+            out_vars=layer_dict["out_vars"],
+            cache=cache_decoded
+        )
 
 
 class NetSerializer:
@@ -213,22 +193,8 @@ def deserialize_net(net_dict: Dict[str, Any], target_device: Optional[str] = Non
         preds = {int(k): v for k, v in graph.get("preds", {}).items()}
         succs = {int(k): v for k, v in graph.get("succs", {}).items()}
         
-        # Create Net object with validation
-        try:
-            return Net(layers=layers, preds=preds, succs=succs)
-        except ValueError as e:
-            # If validation fails during deserialization, create the Net
-            # without validation for template/example usage
-            if "schema violation" in str(e) or "validation" in str(e).lower():
-                print(f"Warning: Creating net without validation")
-                net = object.__new__(Net)
-                net.layers = layers
-                net.preds = preds
-                net.succs = succs
-                net.by_id = {L.id: L for L in layers}
-                return net
-            else:
-                raise
+        # Create Net object with validation; malformed serialized graphs are errors.
+        return Net(layers=layers, preds=preds, succs=succs)
 
 class ACTJSONEncoder(json.JSONEncoder):
     """Custom JSON encoder for ACT objects."""
diff --git a/act/back_end/solver/solver_hz.py b/act/back_end/solver/solver_hz.py
index e3be99a33..c1ddb25dd 100644
--- a/act/back_end/solver/solver_hz.py
+++ b/act/back_end/solver/solver_hz.py
@@ -969,40 +969,18 @@ def softmax_ratio_weighted_extreme(
     ordered_upper = np.take_along_axis(score_upper, order, axis=1).astype(
         np.longdouble
     )
-    shift = np.max(ordered_upper, axis=1, keepdims=True)
-    exp_lower = np.exp(ordered_lower - shift)
-    exp_upper = np.exp(ordered_upper - shift)
-    prefix_num = np.concatenate(
-        [
-            np.zeros((values.shape[0], 1), dtype=np.longdouble),
-            np.cumsum(ordered_objective * exp_upper, axis=1),
-        ],
-        axis=1,
-    )
-    prefix_den = np.concatenate(
-        [
-            np.zeros((values.shape[0], 1), dtype=np.longdouble),
-            np.cumsum(exp_upper, axis=1),
-        ],
-        axis=1,
-    )
-    lower_num = np.concatenate(
-        [
-            np.zeros((values.shape[0], 1), dtype=np.longdouble),
-            np.cumsum(ordered_objective * exp_lower, axis=1),
-        ],
-        axis=1,
-    )
-    lower_den = np.concatenate(
-        [
-            np.zeros((values.shape[0], 1), dtype=np.longdouble),
-            np.cumsum(exp_lower, axis=1),
-        ],
-        axis=1,
-    )
-    candidates = (prefix_num + lower_num[:, -1:] - lower_num) / (
-        prefix_den + lower_den[:, -1:] - lower_den
+    candidates = np.empty(
+        (values.shape[0], values.shape[1] + 1), dtype=np.longdouble
     )
+    for split in range(values.shape[1] + 1):
+        vertex_scores = np.concatenate(
+            [ordered_upper[:, :split], ordered_lower[:, split:]], axis=1
+        )
+        vertex_shift = np.max(vertex_scores, axis=1, keepdims=True)
+        vertex_exp = np.exp(vertex_scores - vertex_shift)
+        candidates[:, split] = np.sum(
+            ordered_objective * vertex_exp, axis=1
+        ) / np.sum(vertex_exp, axis=1)
     vertex = np.asarray(np.min(candidates, axis=1), dtype=np.float64)
     vertex -= 32.0 * np.finfo(np.float64).eps * (1.0 + np.abs(vertex))
     if minimize:
@@ -1548,6 +1526,10 @@ def weighted_mass(capacity, target):
         inequalities = np.empty((signs.shape[0], width + 1), dtype=np.float64)
         inequalities[:, :width] = -signed_weights[row]
         inequalities[:, -1] = -1.0
+        assert np.all(np.isfinite(extrema[row])), (
+            "HybridZ softmax invariant violated: non-finite weighted extrema "
+            f"at row {row}"
+        )
         result = linprog(
             objective,
             A_ub=inequalities,
@@ -2019,7 +2001,7 @@ def _hz_bounds_unconstrained(hz: HZono) -> Bounds:
     return Bounds(lb=(hz.c - rad).reshape(1, -1), ub=(hz.c + rad).reshape(1, -1))
 
 
-def _hz_compute_bounds_scipy(hz: HZono) -> Bounds:
+def _hz_compute_bounds_scipy(hz: HZono) -> Optional[Bounds]:
     model = _lower_hz_milp(hz)
     if model.n_var == 0:
         LB = UB = model.value_center.copy()
@@ -2049,7 +2031,7 @@ def _hz_compute_bounds_scipy(hz: HZono) -> Bounds:
                 options=options,
             )
             if not res_min.success or not res_max.success:
-                raise RuntimeError(f"HybridZ bound MILP failed at output {i}")
+                return None
             LB[i] = model.value_center[i] + res_min.fun
             UB[i] = model.value_center[i] - res_max.fun
 
@@ -2080,11 +2062,9 @@ def hz_compute_bounds(hz: HZono, *, exact: bool = False) -> Bounds:
     if not exact:
         return _hz_bounds_unconstrained(hz)
     if _HAS_SCIPY:
-        try:
-            return _hz_compute_bounds_scipy(hz)
-        except Exception as e:
-            # Intentional: scipy linprog failures fall back to the unconstrained bounds estimate.
-            logger.debug("suppressed: %s", e)
+        exact_bounds = _hz_compute_bounds_scipy(hz)
+        if exact_bounds is not None:
+            return exact_bounds
     return _hz_bounds_unconstrained(hz)
 
 
@@ -2310,21 +2290,17 @@ def _solve_hz_feasibility(
     constraints = (
         LinearConstraint(A, row_lb, row_ub) if A.shape[0] else None
     )
-    try:
-        result = milp(
-            c=np.zeros(model.n_var, dtype=np.float64),
-            integrality=model.integrality,
-            bounds=SciPyBounds(model.var_lb, model.var_ub),
-            constraints=constraints,
-            options={
-                "presolve": True,
-                "time_limit": max(1e-3, remaining),
-                "mip_rel_gap": 0.0,
-            },
-        )
-    except Exception as exc:
-        logger.debug("HybridZ MILP failed: %s", exc)
-        return _MILPResult("unknown", None)
+    result = milp(
+        c=np.zeros(model.n_var, dtype=np.float64),
+        integrality=model.integrality,
+        bounds=SciPyBounds(model.var_lb, model.var_ub),
+        constraints=constraints,
+        options={
+            "presolve": True,
+            "time_limit": max(1e-3, remaining),
+            "mip_rel_gap": 0.0,
+        },
+    )
     nodes = int(getattr(result, "mip_node_count", 0) or 0)
     x = getattr(result, "x", None)
     if x is not None and _valid_milp_point(
@@ -2614,10 +2590,7 @@ def evaluate_spec(
             return self._unknown_results(B, "missing_hz_state")
         if not _HAS_SCIPY:
             return self._unknown_results(B, "scipy_unavailable")
-        try:
-            model = _lower_hz_milp(output_hz)
-        except Exception as exc:
-            return self._unknown_results(B, f"lowering_failed:{type(exc).__name__}")
+        model = _lower_hz_milp(output_hz)
         if model.value_center.size != B * int(n_out):
             return self._unknown_results(B, "output_shape_mismatch")
 
@@ -2642,8 +2615,9 @@ def evaluate_spec(
         if not is_unsafe_linear and highspy is not None:
             try:
                 warm_lp = _HighsLPRelaxation(model)
-            except Exception as exc:
-                logger.debug("HybridZ warm LP setup failed: %s", exc)
+            except RuntimeError:
+                # HiGHS setup can reject a model; MILP remains a sound fallback.
+                warm_lp = None
 
         def solve(extra_A=None, extra_lb=None, extra_ub=None) -> _MILPResult:
             nonlocal solves, nodes
diff --git a/act/back_end/transfer_functions.py b/act/back_end/transfer_functions.py
index fb1294efb..6de1a6df2 100644
--- a/act/back_end/transfer_functions.py
+++ b/act/back_end/transfer_functions.py
@@ -130,15 +130,12 @@ def ensure_active_tf(default_mode: str = "interval") -> TransferFunction:
     """Return the active TF, self-healing to ``default_mode`` if unset.
 
     Consolidates the self-heal pattern shared by analyze.py / cli.py /
-    verifier.py. Catches only ``RuntimeError`` (the documented
-    "not initialised" case); any other exception from a broken TF subclass
-    bubbles up so the bug surfaces rather than silently demoting to interval.
+    verifier.py. Only the "not initialised" state is healed; nothing is
+    caught, so a broken TF subclass surfaces rather than demoting to interval.
     """
-    try:
-        return get_transfer_function()
-    except RuntimeError:
+    if _current_tf is None:
         set_transfer_function_mode(default_mode)
-        return get_transfer_function()
+    return get_transfer_function()
 
 
 def set_transfer_function_mode(mode: str = "interval", tf_config: Any = None) -> None:
@@ -176,10 +173,6 @@ def set_solver_mode(mode: Optional[str]) -> None:
     _current_solver_mode = mode
 
 
-def get_solver_mode() -> Optional[str]:
-    return _current_solver_mode
-
-
 def is_dual_solver_active() -> bool:
     return _current_solver_mode == "dual"
 
diff --git a/act/config/frontend_cli.py b/act/config/frontend_cli.py
index c22ba98c0..e51cc95ee 100644
--- a/act/config/frontend_cli.py
+++ b/act/config/frontend_cli.py
@@ -221,6 +221,7 @@ def print_unified_info(name: str, explicit_creator: Optional[str] = None):
     except ValueError as e:
         print(f"Error: {e}")
         print(f"\nTip: Use --search to find available names or --creator to override detection")
+        raise
 
 
 def handle_unified_download(name: str, explicit_creator: Optional[str] = None):
@@ -243,23 +244,16 @@ def handle_unified_download(name: str, explicit_creator: Optional[str] = None):
             info = tv_mapping.get_dataset_info(normalized_name)
             models = info.get('models', [])
             
-            if not models:
-                print(f"⚠️  No models available for {normalized_name}")
-                return
+            assert models, f"No models available for {normalized_name}"
             
             print(f"Downloading dataset '{normalized_name}' with {len(models)} models...\n")
             
             success_count = 0
             for model in models:
-                try:
-                    result = tv_loader.download_dataset_model_pair(normalized_name, model)
-                    if result['status'] == 'success':
-                        print(f"✓ {normalized_name} + {model}")
-                        success_count += 1
-                    else:
-                        print(f"✗ {normalized_name} + {model} - {result['message']}")
-                except Exception as e:
-                    print(f"✗ {normalized_name} + {model} - Error: {e}")
+                result = tv_loader.download_dataset_model_pair(normalized_name, model)
+                assert result['status'] == 'success', f"{normalized_name} + {model}: {result['message']}"
+                print(f"✓ {normalized_name} + {model}")
+                success_count += 1
             
             print(f"\n{rule(100)}")
             print(f"Downloaded {success_count}/{len(models)} model pairs")
@@ -275,36 +269,29 @@ def handle_unified_download(name: str, explicit_creator: Optional[str] = None):
             print(f"  • VNNLIB property files")
             print(f"  • instances.csv mapping\n")
             
-            try:
-                result = vnnlib_loader.download_vnnlib_category(normalized_name)
-                
-                if result['status'] == 'success':
-                    print(f"\n{rule(100)}")
-                    print(f"✓ Successfully downloaded category: {normalized_name}")
-                    print(f"  Location: {result['category_path']}")
-                    print(f"  Instances: {result['num_instances']}")
-                    print(f"{rule(100)}\n")
-                else:
-                    print(f"\n{rule(100)}")
-                    print(f"✗ Download failed: {result['message']}")
-                    print(f"\nNote: VNNLIB benchmarks must be downloaded manually from VNN-COMP.")
-                    print(f"Expected location: data/vnnlib/{normalized_name}/")
-                    print(f"\nManual download steps:")
-                    print(f"  1. Visit: https://github.com/ChristopherBrix/vnncomp_benchmarks")
-                    print(f"  2. Download the '{normalized_name}' benchmark")
-                    print(f"  3. Extract to: data/vnnlib/{normalized_name}/")
-                    print(f"  4. Ensure structure includes:")
-                    print(f"     - onnx/         (ONNX model files)")
-                    print(f"     - vnnlib/       (VNNLIB property files)")
-                    print(f"     - instances.csv (benchmark instances)")
-                    print(f"{rule(100)}\n")
-                    
-            except Exception as e:
+            result = vnnlib_loader.download_vnnlib_category(normalized_name)
+            
+            if result['status'] != 'success':
                 print(f"\n{rule(100)}")
-                print(f"✗ Download error: {e}")
+                print(f"✗ Download failed: {result['message']}")
                 print(f"\nNote: VNNLIB benchmarks must be downloaded manually from VNN-COMP.")
                 print(f"Expected location: data/vnnlib/{normalized_name}/")
+                print(f"\nManual download steps:")
+                print(f"  1. Visit: https://github.com/ChristopherBrix/vnncomp_benchmarks")
+                print(f"  2. Download the '{normalized_name}' benchmark")
+                print(f"  3. Extract to: data/vnnlib/{normalized_name}/")
+                print(f"  4. Ensure structure includes:")
+                print(f"     - onnx/         (ONNX model files)")
+                print(f"     - vnnlib/       (VNNLIB property files)")
+                print(f"     - instances.csv (benchmark instances)")
                 print(f"{rule(100)}\n")
+            assert result['status'] == 'success', f"Download failed: {result['message']}"
+            
+            print(f"\n{rule(100)}")
+            print(f"✓ Successfully downloaded category: {normalized_name}")
+            print(f"  Location: {result['category_path']}")
+            print(f"  Instances: {result['num_instances']}")
+            print(f"{rule(100)}\n")
         elif creator_name == 'bert':
             print("BERT datasets are file-based.")
             print(f"Expected raw files under data/{normalized_name}/")
@@ -312,6 +299,7 @@ def handle_unified_download(name: str, explicit_creator: Optional[str] = None):
         
     except ValueError as e:
         print(f"Error: {e}")
+        raise
 
 
 def print_list_downloads(creator: Optional[str] = None):
@@ -408,7 +396,7 @@ def print_creator_info(name: str) -> None:
     except ValueError as e:
         print(f"Error: {e}")
         print(f"Available creators: {list_creators()}")
-        return
+        raise
 
     print(f"\n{rule(100)}")
     print(f"CREATOR: {name.upper()}")
@@ -754,28 +742,25 @@ def main():
         print(f"MODEL SYNTHESIS - {creator_name.upper()}")
         print(f"{rule(100)}\n")
         
-        try:
-            from act.front_end.model_synthesis import model_synthesis
-            from act.util.model_inference import model_inference
-            
-            wrapped_models = model_synthesis(
-                creator=creator_name,
-                spec_overrides=_build_spec_overrides(args),
-                text_verification_overrides=_build_text_verification_overrides(args),
-            )
-            print(f"\n✓ Successfully synthesized {len(wrapped_models)} models")
-            
-            # Automatically run inference after synthesis
-            print(f"\n{rule(100)}")
-            print(f"MODEL INFERENCE - {creator_name.upper()}")
-            print(f"{rule(100)}\n")
-            
-            # model_inference extracts input from InputLayer 
-            successful_models = model_inference(cast(Any, wrapped_models))
-            print(f"\n✓ Successfully ran inference on {len(successful_models)}/{len(wrapped_models)} models")
-            print(f"  Models are ready for verification")
-        except Exception as e:
-            print(f"\n✗ Synthesis/Inference failed: {e}")
+        from act.front_end.model_synthesis import model_synthesis
+        from act.util.model_inference import model_inference
+        
+        wrapped_models = model_synthesis(
+            creator=creator_name,
+            spec_overrides=_build_spec_overrides(args),
+            text_verification_overrides=_build_text_verification_overrides(args),
+        )
+        print(f"\n✓ Successfully synthesized {len(wrapped_models)} models")
+        
+        # Automatically run inference after synthesis
+        print(f"\n{rule(100)}")
+        print(f"MODEL INFERENCE - {creator_name.upper()}")
+        print(f"{rule(100)}\n")
+        
+        # model_inference extracts input from InputLayer 
+        successful_models = model_inference(cast(Any, wrapped_models))
+        print(f"\n✓ Successfully ran inference on {len(successful_models)}/{len(wrapped_models)} models")
+        print(f"  Models are ready for verification")
     
     elif args.inference:
         creator_name = args.creator if args.creator else 'torchvision'
@@ -783,86 +768,80 @@ def main():
         print(f"MODEL INFERENCE - {creator_name.upper()}")
         print(f"{rule(100)}\n")
         
-        try:
-            # Get downloaded pairs for the creator
-            downloaded_pairs = []
-            if creator_name == 'torchvision':
-                downloaded_pairs = tv_loader.list_downloaded_pairs()
-            elif creator_name == 'vnnlib':
-                from act.front_end.vnnlib_loader import data_model_loader as vnnlib_loader
-                downloaded_pairs = vnnlib_loader.list_downloaded_pairs()
-            
-            if not downloaded_pairs:
-                print(f"⚠️  No downloaded models found for creator '{creator_name}'")
-                print(f"   Use --download to download datasets/categories first")
-                print(f"   Example: python -m act.front_end --download MNIST --creator {creator_name}")
-            else:
-                print(f"Found {len(downloaded_pairs)} downloaded pair(s) for {creator_name}")
-                print(f"Running inference on downloaded models...\n")
-                
-                results = []
-                
-                # Run inference on each downloaded pair
-                if creator_name == 'torchvision':
-                    for pair_info in downloaded_pairs:
-                        dataset_name = pair_info['dataset']
-                        model_name = pair_info['model']
-                        
-                        # Test the pair
-                        result = tv_loader.model_inference_with_dataset(
-                            dataset_name=dataset_name,
-                            model_name=model_name,
-                            split='test',
-                            verbose=False
-                        )
-                        results.append(result)
-                        
-                        # Print result
-                        if result['status'] == 'success':
-                            print(f"✓ {dataset_name:20s} + {model_name:20s} - Output: {result['output_shape']}")
-                        else:
-                            print(f"✗ {dataset_name:20s} + {model_name:20s} - Error: {result.get('error', 'Unknown')[:50]}")
+        # Get downloaded pairs for the creator
+        downloaded_pairs = []
+        if creator_name == 'torchvision':
+            downloaded_pairs = tv_loader.list_downloaded_pairs()
+        elif creator_name == 'vnnlib':
+            from act.front_end.vnnlib_loader import data_model_loader as vnnlib_loader
+            downloaded_pairs = vnnlib_loader.list_downloaded_pairs()
+        
+        if not downloaded_pairs:
+            print(f"⚠️  No downloaded models found for creator '{creator_name}'")
+            print(f"   Use --download to download datasets/categories first")
+            print(f"   Example: python -m act.front_end --download MNIST --creator {creator_name}")
+        assert downloaded_pairs, f"No downloaded models found for creator '{creator_name}'"
+        print(f"Found {len(downloaded_pairs)} downloaded pair(s) for {creator_name}")
+        print(f"Running inference on downloaded models...\n")
+        
+        results = []
+        
+        # Run inference on each downloaded pair
+        if creator_name == 'torchvision':
+            for pair_info in downloaded_pairs:
+                dataset_name = pair_info['dataset']
+                model_name = pair_info['model']
                 
-                elif creator_name == 'vnnlib':
-                    from act.front_end.vnnlib_loader import data_model_loader as vnnlib_loader
-                    
-                    for pair_info in downloaded_pairs:
-                        category = pair_info['category']
-                        onnx_model = pair_info['onnx_model']
-                        vnnlib_spec = pair_info['vnnlib_spec']
-                        
-                        # Test the pair
-                        result = vnnlib_loader.model_inference_with_vnnlib(
-                            category=category,
-                            onnx_model=onnx_model,
-                            vnnlib_spec=vnnlib_spec,
-                            verbose=False
-                        )
-                        results.append(result)
-                        
-                        # Print result
-                        if result['status'] == 'success':
-                            print(f"✓ {category:20s} + {result['model']:30s} - Output: {result['output_shape']}")
-                        else:
-                            print(f"✗ {category:20s} + {result['model']:30s} - Error: {result.get('error', 'Unknown')[:50]}")
+                # Test the pair
+                result = tv_loader.model_inference_with_dataset(
+                    dataset_name=dataset_name,
+                    model_name=model_name,
+                    split='test',
+                    verbose=False
+                )
+                results.append(result)
                 
-                # Summary
-                successful = sum(1 for r in results if r['status'] == 'success')
-                failed = len(results) - successful
+                # Print result
+                if result['status'] == 'success':
+                    print(f"✓ {dataset_name:20s} + {model_name:20s} - Output: {result['output_shape']}")
+                else:
+                    print(f"✗ {dataset_name:20s} + {model_name:20s} - Error: {result.get('error', 'Unknown')[:50]}")
+        
+        elif creator_name == 'vnnlib':
+            from act.front_end.vnnlib_loader import data_model_loader as vnnlib_loader
+            
+            for pair_info in downloaded_pairs:
+                category = pair_info['category']
+                onnx_model = pair_info['onnx_model']
+                vnnlib_spec = pair_info['vnnlib_spec']
                 
-                print(f"\n{rule(100)}")
-                print(f"INFERENCE SUMMARY")
-                print(f"{rule(100)}")
-                print(f"✓ Successful: {successful}/{len(results)}")
-                if failed > 0:
-                    print(f"✗ Failed: {failed}/{len(results)}")
-                print(f"{rule(100)}\n")
+                # Test the pair
+                result = vnnlib_loader.model_inference_with_vnnlib(
+                    category=category,
+                    onnx_model=onnx_model,
+                    vnnlib_spec=vnnlib_spec,
+                    verbose=False
+                )
+                results.append(result)
                 
-        except Exception as e:
-            import traceback
-            print(f"\n✗ Inference failed: {e}")
-            print(f"\nTraceback:")
-            traceback.print_exc()
+                # Print result
+                if result['status'] == 'success':
+                    print(f"✓ {category:20s} + {result['model']:30s} - Output: {result['output_shape']}")
+                else:
+                    print(f"✗ {category:20s} + {result['model']:30s} - Error: {result.get('error', 'Unknown')[:50]}")
+        
+        # Summary
+        successful = sum(1 for r in results if r['status'] == 'success')
+        failed = len(results) - successful
+        
+        print(f"\n{rule(100)}")
+        print(f"INFERENCE SUMMARY")
+        print(f"{rule(100)}")
+        print(f"✓ Successful: {successful}/{len(results)}")
+        if failed > 0:
+            print(f"✗ Failed: {failed}/{len(results)}")
+        print(f"{rule(100)}\n")
+        assert failed == 0, f"{failed}/{len(results)} inference run(s) failed"
     
     else:
         parser.print_help()
diff --git a/act/config/pipeline_cli.py b/act/config/pipeline_cli.py
index 8a2dbb484..77695d9ce 100644
--- a/act/config/pipeline_cli.py
+++ b/act/config/pipeline_cli.py
@@ -2,6 +2,11 @@
 """
 ACT Pipeline Command-Line Interface.
 
+Exit statuses:
+- 0: command completed successfully
+- 1: runtime, verification, or unexpected error
+- 3: unsupported model/specification
+
 Provides fuzzing capabilities for neural network verification with support for:
 - VNNLib verification benchmarks (default)
 - TorchVision datasets (alternative)
@@ -26,15 +31,18 @@
 logger = logging.getLogger(__name__)
 from act.front_end.specs import OutputSpec
 from act.front_end.vnnlib_loader.create_specs import VNNLibSpecCreator
+from act.front_end.vnnlib_loader.vnnlib_parser import UnsupportedSpecError
 from act.front_end.vnnlib_loader import data_model_loader as vnnlib_loader
-from act.front_end.vnnlib_loader import category_mapping as vnnlib_mapping
 from act.front_end.torchvision_loader.create_specs import TorchVisionSpecCreator
 from act.front_end.torchvision_loader import data_model_loader as tv_loader
-from act.front_end.torchvision_loader import data_model_mapping as tv_mapping
 from act.front_end.model_synthesis import synthesize_models_and_seeds_from_specs
+from act.config.frontend_cli import (
+    print_unified_list, print_unified_search, print_unified_info,
+    handle_unified_download, print_list_downloads,
+)
 from act.pipeline.fuzzing.actfuzzer import ACTFuzzer, FuzzingConfig
 from act.pipeline.verification.per_neuron_bounds import PerNeuronCheckConfig
-from act.config.config import PipelineConfig
+from act.config.config import BackendConfig, PipelineConfig
 
 
 _FUZZ_MUTATION_WEIGHT_KEYS = frozenset(
@@ -271,7 +279,6 @@ def _apply_pipeline_config_defaults(args: Any) -> PipelineConfig:
     return config
 
 
-
 def print_header():
     """Print simple header."""
     print(f"\n{rule()}")
@@ -280,257 +287,12 @@ def print_header():
     print(f"{rule()}\n")
 
 
-# ============================================================================
-# Data-Model Pair Management Commands
-# ============================================================================
-
-
-def cmd_list_available(creator: str):
-    """List available datasets/categories."""
-    print(f"\n{rule()}")
-    print(f"AVAILABLE DATA-MODEL PAIRS ({creator.upper()})")
-    print(f"{rule()}\n")
-
-    if creator == "vnnlib":
-        categories = vnnlib_mapping.list_categories()
-        print(f"VNNLIB Categories ({len(categories)}):")
-        print(rule(80, "-"))
-        for cat_name in sorted(categories):
-            info = vnnlib_mapping.get_category_info(cat_name)
-            print(f"  {cat_name:30s} ({info['type']}) - {info['description']}")
-            print(f"    └─ Models: {info['models']}, Properties: {info['properties']}")
-
-    elif creator == "torchvision":
-        datasets = sorted(tv_mapping.DATASET_MODEL_MAPPING.keys())
-        print(f"TorchVision Datasets ({len(datasets)}):")
-        print(rule(80, "-"))
-        for ds_name in datasets:
-            info = tv_mapping.DATASET_MODEL_MAPPING[ds_name]
-            models = info.get("models", [])
-            print(f"  {ds_name:30s} [{info.get('category', 'N/A')}]")
-            if models:
-                print(
-                    f"    └─ Models: {', '.join(models[:5])}{'...' if len(models) > 5 else ''}"
-                )
-
-    print(f"\n{rule()}\n")
-
-
-def cmd_search(query: str, creator: str):
-    """Search for datasets/categories."""
-    print(f"\n{rule()}")
-    print(f"SEARCH RESULTS: '{query}' ({creator.upper()})")
-    print(f"{rule()}\n")
-
-    if creator == "vnnlib":
-        matches = vnnlib_mapping.search_categories(query)
-        if matches:
-            print(f"Found {len(matches)} VNNLIB categories:")
-            print(rule(80, "-"))
-            for cat_name in sorted(matches):
-                info = vnnlib_mapping.get_category_info(cat_name)
-                print(f"  {cat_name:30s} ({info['type']}) - {info['description']}")
-        else:
-            print(f"No VNNLIB categories found for '{query}'")
-
-    elif creator == "torchvision":
-        matches = tv_mapping.search_datasets(query)
-        if matches:
-            print(f"Found {len(matches)} TorchVision datasets:")
-            print(rule(80, "-"))
-            for ds_name in sorted(matches):
-                info = tv_mapping.DATASET_MODEL_MAPPING[ds_name]
-                print(f"  {ds_name:30s} [{info.get('category', 'N/A')}]")
-        else:
-            print(f"No TorchVision datasets found for '{query}'")
-
-    print(f"\n{rule()}\n")
-
-
-def cmd_info(name: str, creator: str):
-    """Show detailed information about dataset/category."""
-    print(f"\n{rule()}")
-    print(f"INFO: {name} ({creator.upper()})")
-    print(f"{rule()}\n")
-
-    if creator == "vnnlib":
-        try:
-            info = vnnlib_mapping.get_category_info(name)
-            print(f"Category: {name}")
-            print(f"Type: {info['type']}")
-            print(f"Year: {info['year']}")
-            print(f"Description: {info['description']}")
-            print(f"\nModel Information:")
-            print(f"  • Models: {info['models']}")
-            print(f"  • Properties: {info['properties']}")
-            print(f"  • Input Dim: {info['input_dim']}")
-            print(f"  • Output Dim: {info['output_dim']}")
-
-            # Check if downloaded
-            downloaded = vnnlib_loader.list_downloaded_pairs()
-            matching = [p for p in downloaded if p["category"] == name]
-            if matching:
-                print(f"\n✓ Downloaded: {len(matching)} instances")
-            else:
-                print(f"\n⚠ Not downloaded (use --download {name})")
-        except ValueError as e:
-            print(f"Error: {e}")
-
-    elif creator == "torchvision":
-        try:
-            info = tv_mapping.get_dataset_info(name)
-            print(f"Dataset: {name}")
-            print(f"Category: {info.get('category', 'N/A')}")
-            print(f"Input Size: {info.get('input_size', 'N/A')}")
-            print(f"Classes: {info.get('num_classes', 'N/A')}")
-
-            models = info.get("models", [])
-            if models:
-                print(f"\nRecommended Models ({len(models)}):")
-                for model in models:
-                    print(f"  • {model}")
-
-            # Check if downloaded
-            downloaded = tv_loader.list_downloaded_pairs()
-            matching = [p for p in downloaded if p["dataset"] == name]
-            if matching:
-                print(f"\n✓ Downloaded: {len(matching)} model pairs")
-            else:
-                print(
-                    f"\n⚠ Not downloaded (use --download {name} --creator torchvision)"
-                )
-        except ValueError as e:
-            print(f"Error: {e}")
-
-    print(f"\n{rule()}\n")
-
-
-def cmd_download(name: str, creator: str):
-    """Download dataset/category."""
-    print(f"\n{rule()}")
-    print(f"DOWNLOADING: {name} ({creator.upper()})")
-    print(f"{rule()}\n")
-
-    if creator == "vnnlib":
-        try:
-            result = vnnlib_loader.download_vnnlib_category(name)
-
-            if result["status"] == "success":
-                print(f"✓ Successfully downloaded: {name}")
-                print(f"  Location: {result['category_path']}")
-                print(f"  Instances: {result['num_instances']}")
-            else:
-                print(f"✗ Download failed: {result['message']}")
-                print(
-                    f"\nNote: VNNLIB benchmarks must be downloaded manually from VNN-COMP."
-                )
-                print(f"Expected location: data/vnnlib/{name}/")
-                print(f"\nManual steps:")
-                print(
-                    f"  1. Visit: https://github.com/ChristopherBrix/vnncomp_benchmarks"
-                )
-                print(f"  2. Download '{name}' benchmark")
-                print(f"  3. Extract to: data/vnnlib/{name}/")
-                print(f"  4. Ensure structure:")
-                print(f"     - onnx/         (ONNX model files)")
-                print(f"     - vnnlib/       (VNNLIB property files)")
-                print(f"     - instances.csv (benchmark instances)")
-        except Exception as e:
-            print(f"✗ Download error: {e}")
-
-    elif creator == "torchvision":
-        try:
-            info = tv_mapping.get_dataset_info(name)
-            models = info.get("models", [])
-
-            if not models:
-                print(f"⚠ No models available for {name}")
-                return
-
-            print(f"Downloading {name} with {len(models)} models...\n")
-
-            success_count = 0
-            for model in models:
-                result = tv_loader.download_dataset_model_pair(name, model)
-                if result["status"] == "success":
-                    print(f"✓ {name} + {model}")
-                    success_count += 1
-                else:
-                    print(f"✗ {name} + {model} - {result['message']}")
-
-            print(f"\n{rule()}")
-            print(f"Downloaded {success_count}/{len(models)} model pairs")
-            print(f"{rule()}")
-        except Exception as e:
-            print(f"✗ Download error: {e}")
-
-    print()
-
-
-def cmd_list_downloaded(creator: str):
-    """List downloaded data-model pairs."""
-    print(f"\n{rule()}")
-    print(f"DOWNLOADED DATA-MODEL PAIRS ({creator.upper()})")
-    print(f"{rule()}\n")
-
-    if creator == "vnnlib":
-        downloaded = vnnlib_loader.list_downloaded_pairs()
-        if downloaded:
-            # Group by category
-            categories = {}
-            for item in downloaded:
-                cat = item["category"]
-                if cat not in categories:
-                    categories[cat] = []
-                categories[cat].append(item)
-
-            print(f"VNNLIB Downloads ({len(downloaded)} instances):")
-            print(rule(80, "-"))
-            for cat in sorted(categories.keys()):
-                instances = categories[cat]
-                print(f"  {cat:30s} ({len(instances)} instances)")
-                if len(instances) <= 5:
-                    for inst in instances:
-                        print(
-                            f"    └─ {inst['instance_id']}: {inst['onnx_model']} + {inst['vnnlib_spec']}"
-                        )
-        else:
-            print("No VNNLIB downloads found")
-            print("Use --download <category> to download benchmarks")
-
-    elif creator == "torchvision":
-        downloaded = tv_loader.list_downloaded_pairs()
-        if downloaded:
-            # Group by dataset
-            datasets = {}
-            for item in downloaded:
-                ds = item["dataset"]
-                if ds not in datasets:
-                    datasets[ds] = []
-                datasets[ds].append(item["model"])
-
-            print(f"TorchVision Downloads ({len(downloaded)} pairs):")
-            print(rule(80, "-"))
-            for ds in sorted(datasets.keys()):
-                models = datasets[ds]
-                print(f"  {ds:30s} ({len(models)} models)")
-                for model in sorted(models):
-                    print(f"    └─ {model}")
-        else:
-            print("No TorchVision downloads found")
-            print(
-                "Use --download <dataset> --creator torchvision to download data-model pairs"
-            )
-
-    print(f"\n{rule()}\n")
-
-
 # ============================================================================
 # Fuzzing Commands
 # ============================================================================
 
 
-def cmd_fuzz(args):
+def cmd_fuzz(args) -> int:
     """Run ACTFuzzer."""
     print_header()
 
@@ -566,7 +328,7 @@ def cmd_fuzz(args):
                 if not downloaded:
                     print("❌ No VNNLIB categories downloaded!")
                     print("Use: python -m act.pipeline --download <category>")
-                    return
+                    return 1
                 categories = list(set(p["category"] for p in downloaded))
 
             print(f"Loading {len(categories)} VNNLIB category(ies):")
@@ -592,7 +354,7 @@ def cmd_fuzz(args):
                     print(
                         "Use: python -m act.pipeline --download <dataset> --creator torchvision"
                     )
-                    return
+                    return 1
                 datasets = list(set(p["dataset"] for p in downloaded))
 
             print(f"Loading {len(datasets)} TorchVision dataset(s):")
@@ -615,7 +377,7 @@ def cmd_fuzz(args):
 
             if not model_names:
                 print("❌ No models found for selected datasets!")
-                return
+                return 1
 
             spec_results = spec_creator.create_specs_for_data_model_pairs(
                 dataset_names=datasets,
@@ -644,11 +406,11 @@ def cmd_fuzz(args):
         import traceback
 
         traceback.print_exc()
-        return
+        return 1
 
     if not spec_results:
         print("❌ No spec results generated!")
-        return
+        return 1
 
     print(f"✓ Generated {len(spec_results)} spec result(s)\n")
 
@@ -671,11 +433,11 @@ def cmd_fuzz(args):
         import traceback
 
         traceback.print_exc()
-        return
+        return 1
 
     if not wrapped_models:
         print("❌ No models synthesized!")
-        return
+        return 1
 
     print(f"✓ Synthesized {len(wrapped_models)} wrapped model(s)\n")
 
@@ -689,7 +451,7 @@ def cmd_fuzz(args):
 
     if not initial_seeds:
         print("❌ No initial seeds extracted!")
-        return
+        return 1
 
     print(f"✓ Extracted {len(initial_seeds)} initial seeds\n")
 
@@ -722,15 +484,12 @@ def cmd_fuzz(args):
 
         if report.counterexamples and config.save_counterexamples:
             import os
-            import torch as _torch
             from act.front_end.vnnlib_loader.vnnlib_parser import write_vnncomp_result
 
             os.makedirs(config.output_dir, exist_ok=True)
             ce0 = report.counterexamples[0]
-            x = cast(Any, getattr(ce0, "input", ce0))
-            with _torch.no_grad():
-                y_raw = wrapped_model(x)
-            y = cast(Any, y_raw["output"] if isinstance(y_raw, dict) else y_raw)
+            x = ce0.input.unsqueeze(0)
+            y = ce0.output.unsqueeze(0)
             fname = "_".join(map(str, model_id)) if isinstance(model_id, tuple) else str(model_id)
             write_vnncomp_result(
                 os.path.join(config.output_dir, f"{fname}_result.txt"),
@@ -745,7 +504,9 @@ def cmd_fuzz(args):
         import traceback
 
         traceback.print_exc()
-        return
+        return 1
+
+    return 0
 
 
 # ============================================================================
@@ -1023,6 +784,7 @@ def _run_bab_on_net(net, args, bab_first_sample_only: bool = False):
     pipeline_config = PipelineConfig.from_yaml(**_collect_pipeline_config_overrides(args))
     config = pipeline_config.bab
     dual_config = pipeline_config.dual
+    max_batch_size = BackendConfig.from_yaml().bab_max_batch_size
     budget = float(getattr(args, "timeout", 60.0) or 60.0)
 
     spec_layers = gather_input_spec_layers(net)
@@ -1034,7 +796,7 @@ def _run_bab_on_net(net, args, bab_first_sample_only: bool = False):
             net=net,
             solver_factory=TorchLPSolver,
             config=config,
-            max_batch_size=None,
+            max_batch_size=max_batch_size,
             time_budget_s=budget,
             dual_config=dual_config,
         )
@@ -1049,7 +811,7 @@ def _run_bab_on_net(net, args, bab_first_sample_only: bool = False):
                 net=sliced_net,
                 solver_factory=TorchLPSolver,
                 config=config,
-                max_batch_size=None,
+                max_batch_size=max_batch_size,
                 time_budget_s=budget,
                 dual_config=dual_config,
             )
@@ -1285,6 +1047,8 @@ def cmd_verify(target: str, args):
             try:
                 soundness_failed = _run_vnnlib_verify(args)
                 results[test_name] = "FAILED" if soundness_failed else "PASSED"
+            except UnsupportedSpecError:
+                raise
             except Exception as e:
                 print(f"\n❌ Test failed: {e}")
                 import traceback
@@ -1391,6 +1155,11 @@ def main():
   python -m act.pipeline --verify netfactory --solvers torchlp --tf-modes interval --validate-soundness
   python -m act.pipeline --verify vnnlib --category acasxu_2023 --max-instances 3 --validate-soundness
   python -m act.pipeline --verify torchvision --dataset MNIST --model simple_cnn --num-samples 2 --validate-soundness
+
+Exit statuses:
+  0  Command completed successfully
+  1  Runtime, verification, or unexpected error
+  3  Unsupported model/specification
         """,
     )
 
@@ -1784,22 +1553,25 @@ def main():
     # Execute command
     try:
         if args.list:
-            cmd_list_available(args.creator)
+            print_unified_list(args.creator)
         elif args.search:
-            cmd_search(args.search, args.creator)
+            print_unified_search(args.search, args.creator)
         elif args.info:
-            cmd_info(args.info, args.creator)
+            print_unified_info(args.info, explicit_creator=args.creator)
         elif args.download:
-            cmd_download(args.download, args.creator)
+            handle_unified_download(args.download, explicit_creator=args.creator)
         elif args.list_downloaded:
-            cmd_list_downloaded(args.creator)
+            print_list_downloads(args.creator)
         elif args.fuzz:
-            cmd_fuzz(args)
+            sys.exit(cmd_fuzz(args))
         elif args.verify:
             cmd_verify(args.verify, args)
     except KeyboardInterrupt:
         print("\n\n⚠️  Interrupted by user")
         sys.exit(1)
+    except UnsupportedSpecError as e:
+        print(f"\n❌ Unsupported model/specification: {e}")
+        sys.exit(3)
     except Exception as e:
         print(f"\n❌ Error: {e}")
         import traceback
diff --git a/act/front_end/bert_loader/data_loader.py b/act/front_end/bert_loader/data_loader.py
index ff22e42cd..ce74b9d5a 100644
--- a/act/front_end/bert_loader/data_loader.py
+++ b/act/front_end/bert_loader/data_loader.py
@@ -362,7 +362,7 @@ def tokenize(sentence: str) -> list[str]:
         import nltk  # type: ignore[import-untyped]
 
         return nltk.word_tokenize(sentence)
-    except Exception as exc:
+    except (ImportError, LookupError) as exc:  # nltk or its punkt data not installed
         logger.debug("Falling back to regex tokenization: %s", exc)
         return _TOKEN_RE.findall(sentence)
 
diff --git a/act/front_end/spec_creator_base.py b/act/front_end/spec_creator_base.py
index fc713cc0c..3f61178d4 100644
--- a/act/front_end/spec_creator_base.py
+++ b/act/front_end/spec_creator_base.py
@@ -9,7 +9,7 @@
 from __future__ import annotations
 from abc import ABC, abstractmethod
 from dataclasses import dataclass
-from typing import List, Tuple, Dict, Any, Optional, Callable, Union
+from typing import List, Tuple, Dict, Any, Optional, Union
 import logging
 import torch
 
@@ -244,20 +244,7 @@ def __init__(
     
     def _load_config(self, config_name: Optional[str] = None) -> Dict[str, Any]:
         """Load a named spec configuration from the front-end config."""
-        try:
-            return FrontEndConfig.from_yaml().spec_config(config_name)
-        except Exception as e:
-            print(f"⚠️  Could not load config: {e}, using defaults")
-            return self._get_default_config()
-    
-    def _get_default_config(self) -> Dict[str, Any]:
-        """Fallback default configuration"""
-        return {
-            'input_spec_types': ['BOX', 'LINF_BALL'],
-            'output_spec_types': ['MARGIN_ROBUST', 'TOP1_ROBUST'],
-            'perturbation': {'epsilon_values': [0.01, 0.03], 'norm': 'inf'},
-            'combination_strategy': 'balanced'
-        }
+        return FrontEndConfig.from_yaml().spec_config(config_name)
     
     # ==================== SHAPE VALIDATION ==================== #
     
@@ -355,16 +342,12 @@ def validate_spec_pair_with_model(
         errors = []
         
         # Get model I/O shapes
-        try:
-            input_shape, output_shape = self._get_model_io_shapes(model, sample_input)
-            # Assume last dimension is classes for classification
-            if len(output_shape) > 1:
-                num_classes = output_shape[-1]
-            else:
-                num_classes = output_shape[0]
-        except Exception as e:
-            errors.append(f"Failed to infer model shapes: {e}")
-            return False, errors
+        input_shape, output_shape = self._get_model_io_shapes(model, sample_input)
+        # Assume last dimension is classes for classification
+        if len(output_shape) > 1:
+            num_classes = output_shape[-1]
+        else:
+            num_classes = output_shape[0]
         
         # Validate input spec
         input_valid, input_err = self._validate_input_spec_shape(input_spec, input_shape)
@@ -387,19 +370,16 @@ def _validate_and_filter_specs(
         """Validate spec pairs against model and filter invalid ones."""
         valid_pairs = []
         for input_spec, output_spec in spec_pairs:
-            try:
-                is_valid, errors = self.validate_spec_pair_with_model(
-                    input_spec, output_spec, pytorch_model, sample_input
+            is_valid, errors = self.validate_spec_pair_with_model(
+                input_spec, output_spec, pytorch_model, sample_input
+            )
+            if is_valid:
+                valid_pairs.append((input_spec, output_spec))
+            else:
+                logger.debug(
+                    "Spec pair validation failed: %s, %s, with errors:\n%s",
+                    input_spec.kind, output_spec.kind, "\n".join(errors),
                 )
-                if is_valid:
-                    valid_pairs.append((input_spec, output_spec))
-                else:
-                    logger.debug(
-                        "Spec pair validation failed: %s, %s, with errors:\n%s",
-                        input_spec.kind, output_spec.kind, "\n".join(errors),
-                    )
-            except Exception as e:
-                logger.debug("Spec validation error: %s", e)
         return valid_pairs
 
     # ==================== SPEC COMBINATION ==================== #
@@ -439,17 +419,13 @@ def _create_spec_combinations(
     @abstractmethod
     def create_specs_for_data_model_pairs(
         self,
-        max_samples: Optional[int] = None,
-        filter_fn: Optional[Callable] = None,
-        validate_shapes: bool = True
-    ) -> List[Tuple[str, str, torch.nn.Module, List[torch.Tensor], List[Tuple[InputSpec, OutputSpec]]]]:
+        *args: Any,
+        **kwargs: Any,
+    ) -> Any:
         """
         Create specs for data-model pairs (must be implemented by subclasses).
-        
-        Args:
-            max_samples: Maximum number of samples/instances to process
-            filter_fn: Optional filter function (source, model) -> bool
-            validate_shapes: Whether to validate spec shapes with model
+
+        Concrete creators expose source-specific selection and limit options.
         
         Returns:
             List of (data_source, model_name, pytorch_model, input_tensors, spec_pairs) tuples
diff --git a/act/front_end/torchvision_loader/cli.py b/act/front_end/torchvision_loader/cli.py
index e2d48fc83..f7b1b03ac 100644
--- a/act/front_end/torchvision_loader/cli.py
+++ b/act/front_end/torchvision_loader/cli.py
@@ -313,12 +313,14 @@ def main():
                 print(f"  • {name}")
         except ValueError as e:
             print(f"Error: {e}")
+            raise
     
     elif args.dataset:
         try:
             print_dataset_detail(args.dataset)
         except ValueError as e:
             print(f"Error: {e}")
+            raise
     
     elif args.summary:
         print_mapping_summary()
@@ -335,10 +337,7 @@ def main():
             split=args.split
         )
         
-        if result['status'] == 'error':
-            print(f"\n❌ Error: {result['message']}")
-            if 'traceback' in result:
-                print(f"\nDetails:\n{result['traceback']}")
+        assert result['status'] == 'success', f"Download failed: {result['message']}"
         # Success message already printed by download function
     
     elif args.list_downloads:
@@ -432,12 +431,10 @@ def main():
             print(f"✗ Error: {e}")
             print(f"\nThe dataset-model pair has not been downloaded yet.")
             print(f"Use: python -m act.front_end.torchvision_loader.cli --download {dataset_name} {model_name}")
+            raise
         except ValueError as e:
             print(f"✗ Error: {e}")
-        except Exception as e:
-            print(f"✗ Unexpected error: {e}")
-            import traceback
-            print(f"\nDetails:\n{traceback.format_exc()}")
+            raise
     
     elif args.models_for:
         # Show all recommended models for a dataset (case-insensitive)
@@ -497,6 +494,7 @@ def main():
         except ValueError as e:
             print(f"Error: {e}")
             print(f"Use --list to see all available datasets")
+            raise
     
     elif args.datasets_for:
         # Show all datasets that can run inference with a model (case-insensitive)
@@ -603,18 +601,17 @@ def main():
                     print(f"  Dataset samples: {result['num_samples']}")
             
             print(f"{rule()}")
+            assert result['status'] == 'success', f"Inference failed: {result.get('error')}"
             
         except FileNotFoundError as e:
             print(f"\n✗ Error: Dataset-model pair not found locally")
             print(f"   {e}")
             print(f"\nDownload first with:")
             print(f"   python -m act.front_end.torchvision_loader.cli --download {dataset_name} {model_name}")
+            raise
         except ValueError as e:
             print(f"\n✗ Error: {e}")
-        except Exception as e:
-            print(f"\n✗ Unexpected error: {e}")
-            import traceback
-            print(f"\nDetails:\n{traceback.format_exc()}")
+            raise
     
     elif args.validate:
         user_dataset, user_model = args.validate
@@ -643,6 +640,7 @@ def main():
             print(f"{rule(100)}")
         except ValueError as e:
             print(f"Error: {e}")
+            raise
     
     elif args.show_preprocessing:
         try:
@@ -677,6 +675,7 @@ def main():
             print(f"{rule(100)}")
         except ValueError as e:
             print(f"Error: {e}")
+            raise
     
     else:
         # Default: show quick examples
diff --git a/act/front_end/torchvision_loader/create_specs.py b/act/front_end/torchvision_loader/create_specs.py
index 7a75506ca..a3a511f4f 100644
--- a/act/front_end/torchvision_loader/create_specs.py
+++ b/act/front_end/torchvision_loader/create_specs.py
@@ -135,6 +135,7 @@ def create_specs_for_data_model_pairs(
         logger.info(f"Processing {len(all_pairs)} dataset-model pairs")
         
         results = []
+        failures: List[str] = []
         
         for pair_info in all_pairs:
             dataset_name = pair_info['dataset']
@@ -166,8 +167,7 @@ def create_specs_for_data_model_pairs(
                     validate_shapes=validate_shapes
                 )
                 
-                if result is not None:
-                    results.append(result)
+                results.append(result)
                 
                 # Memory optimization: Free dataset/dataloader after extracting input_tensors
                 # pair_data contains the dataset (476 MB for MNIST) which is no longer needed
@@ -175,11 +175,17 @@ def create_specs_for_data_model_pairs(
                 del pair_data, dataloader
                 gc.collect()
                 
-            except Exception as e:
+            except Exception as e:  # noqa: BLE001 — collect every failure, raise below
                 logger.error(
                     f"Failed to create specs for {dataset_name} + {model_name}: {e}"
                 )
+                failures.append(f"{dataset_name} + {model_name}: {e}")
         
+        if failures:
+            raise RuntimeError(
+                f"Spec creation failed for {len(failures)}/{len(all_pairs)} dataset-model pair(s):\n  "
+                + "\n  ".join(failures)
+            )
         logger.info(f"Successfully created specs for {len(results)} pairs")
         return results
     
@@ -192,7 +198,7 @@ def _create_specs_for_single_instance(
         num_samples: int,
         start_index: int,
         validate_shapes: bool
-    ) -> Optional[Tuple[str, str, nn.Module, List[LabeledInputTensor], List[Tuple[InputSpec, OutputSpec]]]]:
+    ) -> Tuple[str, str, nn.Module, List[LabeledInputTensor], List[Tuple[InputSpec, OutputSpec]]]:
         """
         Create specs for a single dataset-model pair.
         
@@ -218,8 +224,7 @@ def _create_specs_for_single_instance(
             labeled_tensors.append(LabeledInputTensor(tensor=tensor, label=label))
         
         if not labeled_tensors:
-            logger.warning(f"No samples collected for {data_source}")
-            return None
+            raise RuntimeError(f"No samples collected for {data_source} + {model_name}")
         
         logger.info(f"Collected {len(labeled_tensors)} samples")
         
@@ -261,8 +266,7 @@ def _create_specs_for_single_instance(
             spec_pairs = validated_pairs
         
         if not spec_pairs:
-            logger.warning(f"No valid specs generated for {data_source} + {model_name}")
-            return None
+            raise RuntimeError(f"No valid specs generated for {data_source} + {model_name}")
         
         return (data_source, model_name, pytorch_model, labeled_tensors, spec_pairs)
     
diff --git a/act/front_end/torchvision_loader/data_model_loader.py b/act/front_end/torchvision_loader/data_model_loader.py
index 22e7132aa..e05cbad9c 100644
--- a/act/front_end/torchvision_loader/data_model_loader.py
+++ b/act/front_end/torchvision_loader/data_model_loader.py
@@ -131,19 +131,14 @@ def _download_dataset(
         # Archive datasets ship train+test in one archive: download
         # once, then both splits are available regardless of `split`.
         print(f"  • Downloading archive from {dataset_info['download']['url']} ...")
-        try:
-            for split_name in ('test', 'train'):
-                ds = _resolve_external_dataset(
-                    dataset_info, raw_dir,
-                    train=(split_name == 'train'),
-                    download=True,
-                )
-                downloaded_splits.append(split_name)
-                print(f"    ✓ {split_name.capitalize()} split: {len(ds)} samples")
-        except Exception as e:
-            error = f"External archive download failed: {e}"
-            errors.append(error)
-            print("    ⚠ " + error)
+        for split_name in ('test', 'train'):
+            ds = _resolve_external_dataset(
+                dataset_info, raw_dir,
+                train=(split_name == 'train'),
+                download=True,
+            )
+            downloaded_splits.append(split_name)
+            print(f"    ✓ {split_name.capitalize()} split: {len(ds)} samples")
     else:
         import torchvision.datasets
         dataset_class = getattr(torchvision.datasets, dataset_name, None)
@@ -159,19 +154,14 @@ def _download_dataset(
             if split not in (split_name, 'both'):
                 continue
             print(f"  • Downloading {split_name} split...")
-            try:
-                # Split-selection kwarg differs per dataset (train= / split= / image_set= / version= / background= / none), so unpack the per-dataset set declared in split_kwarg.
-                ds = dataset_class(
-                    root=str(raw_dir),
-                    **dataset_info["split_kwarg"][split_name],
-                    download=True
-                )
-                downloaded_splits.append(split_name)
-                print(f"    ✓ {split_name.capitalize()} split: {len(ds)} samples")
-            except Exception as e:
-                error = f"{split_name.capitalize()} split failed: {e}"
-                errors.append(error)
-                print("    ⚠ " + error)
+            # Split-selection kwarg differs per dataset (train= / split= / image_set= / version= / background= / none), so unpack the per-dataset set declared in split_kwarg.
+            ds = dataset_class(
+                root=str(raw_dir),
+                **dataset_info["split_kwarg"][split_name],
+                download=True
+            )
+            downloaded_splits.append(split_name)
+            print(f"    ✓ {split_name.capitalize()} split: {len(ds)} samples")
     
     return downloaded_splits, errors
 
@@ -211,98 +201,93 @@ def download_dataset_model_pair(
         >>> print(result['dataset_path'])
         '/path/to/ACT/data/torchvision/MNIST/raw/'
     """
-    import traceback
-    
     # Use path from config if not specified
     if root_dir is None:
         root_dir = get_torchvision_data_root()
     
-    try:
-        # Normalize names (case-insensitive)
-        dataset_name = find_dataset_name(dataset_name)
-        model_name = find_model_name(model_name)
-        
-        # Validate compatibility
-        validation = validate_dataset_model_compatibility(dataset_name, model_name)
-        if not validation['compatible']:
+    # Normalize names (case-insensitive)
+    dataset_name = find_dataset_name(dataset_name)
+    model_name = find_model_name(model_name)
+    
+    # Validate compatibility
+    validation = validate_dataset_model_compatibility(dataset_name, model_name)
+    if not validation['compatible']:
+        return {
+            'status': 'error',
+            'message': f"Incompatible pair: {', '.join(validation['issues'])}"
+        }
+    
+    # Get dataset info
+    dataset_info = get_dataset_info(dataset_name)
+    
+    # Create directory structure
+    dataset_dir = Path(root_dir) / dataset_name
+    raw_dir = dataset_dir / "raw"
+    models_dir = dataset_dir / "models"
+    
+    # Check if dataset already exists (for incremental download)
+    dataset_exists = dataset_dir.exists() and raw_dir.exists()
+    model_file_path = models_dir / f"{model_name}.py"
+    model_already_exists = model_file_path.exists()
+    
+    if dataset_exists:
+        if model_already_exists:
+            print(f"\n⚠️  Model '{model_name}' already exists for dataset '{dataset_name}'")
+            print(f"   Skipping download (pair already complete)")
             return {
-                'status': 'error',
-                'message': f"Incompatible pair: {', '.join(validation['issues'])}"
+                'status': 'success',
+                'message': f"Model {model_name} already exists for {dataset_name}",
+                'path': str(dataset_dir)
             }
-        
-        # Get dataset info
-        dataset_info = get_dataset_info(dataset_name)
-        
-        # Create directory structure
-        dataset_dir = Path(root_dir) / dataset_name
-        raw_dir = dataset_dir / "raw"
-        models_dir = dataset_dir / "models"
-        
-        # Check if dataset already exists (for incremental download)
-        dataset_exists = dataset_dir.exists() and raw_dir.exists()
-        model_file_path = models_dir / f"{model_name}.py"
-        model_already_exists = model_file_path.exists()
-        
-        if dataset_exists:
-            if model_already_exists:
-                print(f"\n⚠️  Model '{model_name}' already exists for dataset '{dataset_name}'")
-                print(f"   Skipping download (pair already complete)")
-                return {
-                    'status': 'success',
-                    'message': f"Model {model_name} already exists for {dataset_name}",
-                    'path': str(dataset_dir)
-                }
-            else:
-                print(f"\n✓ Dataset '{dataset_name}' already downloaded - adding model '{model_name}'")
-                print(f"  Location: {raw_dir}")
-                
-                # Load existing metadata to check splits
-                info_path = dataset_dir / "info.json"
-                if info_path.exists():
-                    with open(info_path, 'r') as f:
-                        existing_metadata = json.load(f)
-                    downloaded_splits = existing_metadata.get('splits_downloaded', [])
-                    print(f"  Existing splits: {', '.join(downloaded_splits)}")
-                else:
-                    downloaded_splits = []
-                
-                # Create models directory if it doesn't exist
-                models_dir.mkdir(parents=True, exist_ok=True)
         else:
-            # Fresh download - create directories
-            raw_dir.mkdir(parents=True, exist_ok=True)
+            print(f"\n✓ Dataset '{dataset_name}' already downloaded - adding model '{model_name}'")
+            print(f"  Location: {raw_dir}")
+            
+            # Load existing metadata to check splits
+            info_path = dataset_dir / "info.json"
+            if info_path.exists():
+                with open(info_path, 'r') as f:
+                    existing_metadata = json.load(f)
+                downloaded_splits = existing_metadata.get('splits_downloaded', [])
+                print(f"  Existing splits: {', '.join(downloaded_splits)}")
+            else:
+                downloaded_splits = []
+            
+            # Create models directory if it doesn't exist
             models_dir.mkdir(parents=True, exist_ok=True)
-            downloaded_splits = []
-        
-        print(f"\n{rule()}")
-        print(f"{'ADDING MODEL' if dataset_exists else 'DOWNLOADING'}: {dataset_name} + {model_name}")
-        print(f"{rule()}")
-        print(f"Target: {dataset_dir}")
-        if not dataset_exists:
-            print(f"Split: {split}")
-        
-        # Download dataset (only if not already present)
-        if not dataset_exists:
-            print(f"\n[1/3] Downloading dataset...")
+    else:
+        # Fresh download - create directories
+        raw_dir.mkdir(parents=True, exist_ok=True)
+        models_dir.mkdir(parents=True, exist_ok=True)
+        downloaded_splits = []
+    
+    print(f"\n{rule()}")
+    print(f"{'ADDING MODEL' if dataset_exists else 'DOWNLOADING'}: {dataset_name} + {model_name}")
+    print(f"{rule()}")
+    print(f"Target: {dataset_dir}")
+    if not dataset_exists:
+        print(f"Split: {split}")
+    
+    # Download dataset (only if not already present)
+    if not dataset_exists:
+        print(f"\n[1/3] Downloading dataset...")
 
-            downloaded_splits, errors = _download_dataset(root_dir, dataset_name, dataset_info, split)
+        downloaded_splits, errors = _download_dataset(root_dir, dataset_name, dataset_info, split)
 
-            if not downloaded_splits:
-                return {
-                    'status': 'error',
-                    'message': f"Failed to download any splits for {dataset_name}, with errors: {"\n".join(errors)}"
-                }
-        else:
-            print(f"\n[1/3] Dataset already present, skipping download...")
-        
-        # Save model architecture
-        print(f"\n[2/3] Saving model architecture...")
-        model_path = models_dir / f"{model_name}.py"
-        
-        import torchvision.models
-        if hasattr(torchvision.models, model_name):
-            # Standard TorchVision model
-            model_code = f"""
+        assert downloaded_splits and not errors, (
+            f"Failed to download {dataset_name}: {'; '.join(errors)}"
+        )
+    else:
+        print(f"\n[1/3] Dataset already present, skipping download...")
+    
+    # Save model architecture
+    print(f"\n[2/3] Saving model architecture...")
+    model_path = models_dir / f"{model_name}.py"
+    
+    import torchvision.models
+    if hasattr(torchvision.models, model_name):
+        # Standard TorchVision model
+        model_code = f"""
 # Standard TorchVision Model: {model_name}
 # Can be loaded with: torchvision.models.{model_name}()
 
@@ -321,106 +306,92 @@ def download_dataset_model_pair(
 print(f"Model: {model_name}")
 print(f"Parameters: {{sum(p.numel() for p in model.parameters()):,}}")
 """
-        else:
-            # Custom model - get definition
-            model_code = _get_custom_model_definition(model_name, dataset_info['num_classes'])
-        
-        with open(model_path, 'w') as f:
-            f.write(model_code)
-        print(f"  ✓ Model architecture saved: {model_path}")
-        
-        # Save/update metadata
-        print(f"\n[3/3] Saving metadata...")
-        info_path = dataset_dir / "info.json"
+    else:
+        # Custom model - get definition
+        model_code = _get_custom_model_definition(model_name, dataset_info['num_classes'])
+    
+    with open(model_path, 'w') as f:
+        f.write(model_code)
+    print(f"  ✓ Model architecture saved: {model_path}")
+    
+    # Save/update metadata
+    print(f"\n[3/3] Saving metadata...")
+    info_path = dataset_dir / "info.json"
+    
+    # Load existing metadata if it exists
+    if info_path.exists():
+        with open(info_path, 'r') as f:
+            existing_metadata = json.load(f)
         
-        # Load existing metadata if it exists
-        if info_path.exists():
-            try:
-                with open(info_path, 'r') as f:
-                    existing_metadata = json.load(f)
-                
-                # Check if this is old format (single model) or new format (list of models)
-                if 'models' not in existing_metadata:
-                    # Old format - convert to new format
-                    old_model = existing_metadata.get('model')
-                    models_list = [old_model] if old_model else []
-                else:
-                    models_list = existing_metadata.get('models', [])
-                
-                # Add new model if not already in list
-                if model_name not in models_list:
-                    models_list.append(model_name)
-                
-                # Preserve existing splits if incremental
-                if dataset_exists:
-                    downloaded_splits = existing_metadata.get('splits_downloaded', downloaded_splits)
-            except Exception as e:
-                print(f"  ⚠ Could not read existing metadata: {e}")
-                models_list = [model_name]
+        # Check if this is old format (single model) or new format (list of models)
+        if 'models' not in existing_metadata:
+            # Old format - convert to new format
+            old_model = existing_metadata.get('model')
+            models_list = [old_model] if old_model else []
         else:
-            models_list = [model_name]
-        
-        # Create updated metadata with list of models
-        metadata = {
-            'dataset': dataset_name,
-            'models': models_list,  # Changed from single 'model' to list 'models'
-            'category': dataset_info['category'],
-            'input_size': dataset_info['input_size'],
-            'num_classes': dataset_info['num_classes'],
-            'splits_downloaded': downloaded_splits,
-            'preprocessing_required': validation['preprocessing_required'],
-            'preprocessing_steps': validation['preprocessing_steps'],
-            'notes': dataset_info['notes'],
-            'paths': {
-                'raw_data': str(raw_dir),
-                'models_directory': str(models_dir),
-                'metadata': str(info_path)
-            }
-        }
+            models_list = existing_metadata.get('models', [])
         
-        with open(info_path, 'w') as f:
-            json.dump(metadata, f, indent=2)
-        print(f"  ✓ Metadata saved: {info_path}")
-        print(f"  ✓ Models registered: {', '.join(models_list)}")
+        # Add new model if not already in list
+        if model_name not in models_list:
+            models_list.append(model_name)
         
-        # Calculate directory size
-        total_size_bytes = _get_directory_size(dataset_dir)
-        total_size_formatted = _format_size(total_size_bytes)
-        
-        # Print summary
-        print(f"\n{rule()}")
-        print(f"✓ DOWNLOAD COMPLETE")
-        print(f"{rule()}")
-        print(f"Dataset: {raw_dir}")
-        print(f"Model: {model_path}")
-        print(f"Info: {info_path}")
-        print(f"Size: {total_size_formatted} ({total_size_bytes:,} bytes)")
-        
-        if validation['preprocessing_required']:
-            print(f"\n⚠ Preprocessing Required:")
-            for step in validation['preprocessing_steps']:
-                print(f"  • {step}")
-        
-        return {
-            'status': 'success',
-            'dataset_path': str(raw_dir),
-            'model_path': str(model_path),
-            'info_path': str(info_path),
-            'message': 'Download completed successfully',
-            'metadata': metadata,
-            'size_bytes': total_size_bytes,
-            'size_formatted': total_size_formatted
-        }
-        
-    except AssertionError:
-        # Re-raise AssertionError from validation without catching
-        raise
-    except Exception as e:
-        return {
-            'status': 'error',
-            'message': f"Download failed: {str(e)}",
-            'traceback': traceback.format_exc()
+        # Preserve existing splits if incremental
+        if dataset_exists:
+            downloaded_splits = existing_metadata.get('splits_downloaded', downloaded_splits)
+    else:
+        models_list = [model_name]
+    
+    # Create updated metadata with list of models
+    metadata = {
+        'dataset': dataset_name,
+        'models': models_list,  # Changed from single 'model' to list 'models'
+        'category': dataset_info['category'],
+        'input_size': dataset_info['input_size'],
+        'num_classes': dataset_info['num_classes'],
+        'splits_downloaded': downloaded_splits,
+        'preprocessing_required': validation['preprocessing_required'],
+        'preprocessing_steps': validation['preprocessing_steps'],
+        'notes': dataset_info['notes'],
+        'paths': {
+            'raw_data': str(raw_dir),
+            'models_directory': str(models_dir),
+            'metadata': str(info_path)
         }
+    }
+    
+    with open(info_path, 'w') as f:
+        json.dump(metadata, f, indent=2)
+    print(f"  ✓ Metadata saved: {info_path}")
+    print(f"  ✓ Models registered: {', '.join(models_list)}")
+    
+    # Calculate directory size
+    total_size_bytes = _get_directory_size(dataset_dir)
+    total_size_formatted = _format_size(total_size_bytes)
+    
+    # Print summary
+    print(f"\n{rule()}")
+    print(f"✓ DOWNLOAD COMPLETE")
+    print(f"{rule()}")
+    print(f"Dataset: {raw_dir}")
+    print(f"Model: {model_path}")
+    print(f"Info: {info_path}")
+    print(f"Size: {total_size_formatted} ({total_size_bytes:,} bytes)")
+    
+    if validation['preprocessing_required']:
+        print(f"\n⚠ Preprocessing Required:")
+        for step in validation['preprocessing_steps']:
+            print(f"  • {step}")
+    
+    return {
+        'status': 'success',
+        'dataset_path': str(raw_dir),
+        'model_path': str(model_path),
+        'info_path': str(info_path),
+        'message': 'Download completed successfully',
+        'metadata': metadata,
+        'size_bytes': total_size_bytes,
+        'size_formatted': total_size_formatted
+    }
 
 
 def list_downloaded_pairs(root_dir: Optional[str] = None) -> List[dict]:
@@ -455,46 +426,42 @@ def list_downloaded_pairs(root_dir: Optional[str] = None) -> List[dict]:
         if not info_path.exists():
             continue
         
-        try:
-            with open(info_path, 'r') as f:
-                metadata = json.load(f)
-            
-            # Calculate directory size (once per dataset)
-            size_bytes = _get_directory_size(dataset_dir)
-            size_formatted = _format_size(size_bytes)
-            
-            # info.json may store either a list under 'models' or a single
-            # 'model' string; normalise both into models_list.
-            if 'models' in metadata:
-                models_list = metadata['models']
-            else:
-                model = metadata.get('model')
-                models_list = [model] if model else []
-            
-            # Create one entry per model
-            for model_name in models_list:
-                pair_metadata = {
-                    'dataset': metadata['dataset'],
-                    'model': model_name,
-                    'category': metadata.get('category', 'unknown'),
-                    'input_size': metadata.get('input_size', []),
-                    'num_classes': metadata.get('num_classes', 0),
-                    'splits_downloaded': metadata.get('splits_downloaded', []),
-                    'preprocessing_required': metadata.get('preprocessing_required', True),
-                    'preprocessing_steps': metadata.get('preprocessing_steps', []),
-                    'notes': metadata.get('notes', ''),
-                    'paths': {
-                        'raw_data': metadata['paths'].get('raw_data', ''),
-                        'model_architecture': str(dataset_dir / "models" / f"{model_name}.py"),
-                        'metadata': str(info_path)
-                    },
-                    'size_bytes': size_bytes,
-                    'size_formatted': size_formatted
-                }
-                downloaded.append(pair_metadata)
-                
-        except Exception as e:
-            print(f"Warning: Could not read {info_path}: {e}")
+        with open(info_path, 'r') as f:
+            metadata = json.load(f)
+        
+        # Calculate directory size (once per dataset)
+        size_bytes = _get_directory_size(dataset_dir)
+        size_formatted = _format_size(size_bytes)
+        
+        # info.json may store either a list under 'models' or a single
+        # 'model' string; normalise both into models_list.
+        if 'models' in metadata:
+            models_list = metadata['models']
+        else:
+            model = metadata.get('model')
+            models_list = [model] if model else []
+        
+        # Create one entry per model
+        for model_name in models_list:
+            pair_metadata = {
+                'dataset': metadata['dataset'],
+                'model': model_name,
+                'category': metadata.get('category', 'unknown'),
+                'input_size': metadata.get('input_size', []),
+                'num_classes': metadata.get('num_classes', 0),
+                'splits_downloaded': metadata.get('splits_downloaded', []),
+                'preprocessing_required': metadata.get('preprocessing_required', True),
+                'preprocessing_steps': metadata.get('preprocessing_steps', []),
+                'notes': metadata.get('notes', ''),
+                'paths': {
+                    'raw_data': metadata['paths'].get('raw_data', ''),
+                    'model_architecture': str(dataset_dir / "models" / f"{model_name}.py"),
+                    'metadata': str(info_path)
+                },
+                'size_bytes': size_bytes,
+                'size_formatted': size_formatted
+            }
+            downloaded.append(pair_metadata)
     
     return downloaded
 
@@ -761,114 +728,88 @@ def model_inference_with_dataset(
     
     combo_id = f"m:{model_name}|x:{dataset_name}|split:{split}"
     
-    try:
-        # Load the pair
-        if verbose:
-            print(f"Testing: {dataset_name} + {model_name} ({split} split)")
-        
-        result = load_dataset_model_pair(
-            dataset_name=dataset_name,
-            model_name=model_name,
-            split=split,
-            batch_size=1,
-            shuffle=False,
-            auto_download=True,
-            root_dir=root_dir
-        )
-        
-        model = result['model']
-        dataloader = result['dataloader']
-        num_samples = result['num_samples']
-        
-        # Get first sample to test
-        input_tensor = None
-        try:
-            for batch in dataloader:
-                if isinstance(batch, (tuple, list)) and len(batch) >= 2:
-                    # Standard (image, label) tuple
-                    input_tensor, labels = batch[0], batch[1]
-                elif isinstance(batch, (tuple, list)) and len(batch) == 1:
-                    input_tensor = batch[0]
-                else:
-                    input_tensor = batch
-                break  # Only need first batch
-        except Exception as e:
-            error_msg = f'Batch loading error: {str(e)[:50]}'
-            if verbose:
-                print(f"  ✗ FAILED - {error_msg}")
-            return {
-                'dataset': dataset_name,
-                'model': model_name,
-                'split': split,
-                'status': 'failed',
-                'error': error_msg,
-                'num_samples': num_samples
-            }
-        
-        if input_tensor is None:
-            error_msg = 'Empty dataloader'
-            if verbose:
-                print(f"  ✗ FAILED - {error_msg}")
-            return {
-                'dataset': dataset_name,
-                'model': model_name,
-                'split': split,
-                'status': 'failed',
-                'error': error_msg,
-                'num_samples': num_samples
-            }
-        
-        # Verify we have a tensor
-        if not isinstance(input_tensor, torch.Tensor):
-            error_msg = f'Input type {type(input_tensor).__name__}, expected torch.Tensor'
-            if verbose:
-                print(f"  ✗ FAILED - {error_msg}")
-            return {
-                'dataset': dataset_name,
-                'model': model_name,
-                'split': split,
-                'status': 'failed',
-                'error': error_msg,
-                'num_samples': num_samples
-            }
-        
-        # Run inference
-        success, output, error_msg = infer_single_model(combo_id, model, input_tensor)
-        
-        if success:
-            output_shape = tuple(output.shape) if output is not None else None
-            if verbose:
-                print(f"  ✓ SUCCESS - Output shape: {output_shape}")
-            return {
-                'dataset': dataset_name,
-                'model': model_name,
-                'split': split,
-                'status': 'success',
-                'output_shape': output_shape,
-                'num_samples': num_samples
-            }
+    # Load the pair
+    if verbose:
+        print(f"Testing: {dataset_name} + {model_name} ({split} split)")
+    
+    result = load_dataset_model_pair(
+        dataset_name=dataset_name,
+        model_name=model_name,
+        split=split,
+        batch_size=1,
+        shuffle=False,
+        auto_download=True,
+        root_dir=root_dir
+    )
+    
+    model = result['model']
+    dataloader = result['dataloader']
+    num_samples = result['num_samples']
+    
+    # Get first sample to test
+    input_tensor = None
+    for batch in dataloader:
+        if isinstance(batch, (tuple, list)) and len(batch) >= 2:
+            # Standard (image, label) tuple
+            input_tensor, labels = batch[0], batch[1]
+        elif isinstance(batch, (tuple, list)) and len(batch) == 1:
+            input_tensor = batch[0]
         else:
-            if verbose:
-                print(f"  ✗ FAILED - {error_msg}")
-            return {
-                'dataset': dataset_name,
-                'model': model_name,
-                'split': split,
-                'status': 'failed',
-                'error': error_msg,
-                'num_samples': num_samples
-            }
-            
-    except Exception as e:
-        error_msg = str(e)[:100]
+            input_tensor = batch
+        break  # Only need first batch
+    
+    if input_tensor is None:
+        error_msg = 'Empty dataloader'
         if verbose:
-            print(f"  ✗ ERROR - {error_msg}")
+            print(f"  ✗ FAILED - {error_msg}")
         return {
             'dataset': dataset_name,
             'model': model_name,
             'split': split,
-            'status': 'error',
-            'error': error_msg
+            'status': 'failed',
+            'error': error_msg,
+            'num_samples': num_samples
+        }
+    
+    # Verify we have a tensor
+    if not isinstance(input_tensor, torch.Tensor):
+        error_msg = f'Input type {type(input_tensor).__name__}, expected torch.Tensor'
+        if verbose:
+            print(f"  ✗ FAILED - {error_msg}")
+        return {
+            'dataset': dataset_name,
+            'model': model_name,
+            'split': split,
+            'status': 'failed',
+            'error': error_msg,
+            'num_samples': num_samples
+        }
+    
+    # Run inference
+    success, output, error_msg = infer_single_model(combo_id, model, input_tensor)
+    
+    if success:
+        output_shape = tuple(output.shape) if output is not None else None
+        if verbose:
+            print(f"  ✓ SUCCESS - Output shape: {output_shape}")
+        return {
+            'dataset': dataset_name,
+            'model': model_name,
+            'split': split,
+            'status': 'success',
+            'output_shape': output_shape,
+            'num_samples': num_samples
+        }
+    else:
+        if verbose:
+            print(f"  ✗ FAILED - {error_msg}")
+        return {
+            'dataset': dataset_name,
+            'model': model_name,
+            'split': split,
+            'status': 'failed',
+            'error': error_msg,
+            'num_samples': num_samples
         }
 
 
@@ -957,6 +898,7 @@ def main():
             print(f"   • {pair_key}: {reason}")
     
     print(rule())
+    assert failed_pairs == 0, f"{failed_pairs}/{total_pairs} dataset-model pair(s) failed inference"
 
 
 if __name__ == "__main__":
diff --git a/act/front_end/vnnlib_loader/cli.py b/act/front_end/vnnlib_loader/cli.py
index 6781275de..4efd17700 100644
--- a/act/front_end/vnnlib_loader/cli.py
+++ b/act/front_end/vnnlib_loader/cli.py
@@ -102,6 +102,7 @@ def print_category_detail(category_name: str):
         
     except ValueError as e:
         print(f"Error: {e}")
+        raise
 
 
 def print_summary_statistics():
@@ -206,6 +207,7 @@ def main():
         except ValueError as e:
             print(f"Error: {e}")
             print(f"\nAvailable types: {', '.join(get_all_types())}")
+            raise
     
     elif args.info:
         print_category_detail(args.info)
@@ -261,24 +263,25 @@ def main():
                 force_redownload=args.force
             )
             
-            if result['status'] == 'success':
-                print(f"\n{rule(100)}")
-                print(f"✓ DOWNLOAD SUCCESSFUL")
-                print(f"{rule(100)}")
-                print(f"Category: {actual_name}")
-                print(f"Path: {result['category_path']}")
-                print(f"Instances: {result['num_instances']}")
-                if 'num_onnx_models' in result:
-                    print(f"ONNX models: {result['num_onnx_models']}")
-                if 'num_vnnlib_specs' in result:
-                    print(f"VNNLIB specs: {result['num_vnnlib_specs']}")
-                print(f"{rule(100)}\n")
-            else:
+            if result['status'] != 'success':
                 print(f"\n{rule(100)}")
                 print(f"⚠️  DOWNLOAD FAILED")
                 print(f"{rule(100)}")
                 print(f"Error: {result.get('message', 'Unknown error')}")
                 print(f"{rule(100)}\n")
+            assert result['status'] == 'success', f"Download failed: {result.get('message')}"
+            
+            print(f"\n{rule(100)}")
+            print(f"✓ DOWNLOAD SUCCESSFUL")
+            print(f"{rule(100)}")
+            print(f"Category: {actual_name}")
+            print(f"Path: {result['category_path']}")
+            print(f"Instances: {result['num_instances']}")
+            if 'num_onnx_models' in result:
+                print(f"ONNX models: {result['num_onnx_models']}")
+            if 'num_vnnlib_specs' in result:
+                print(f"VNNLIB specs: {result['num_vnnlib_specs']}")
+            print(f"{rule(100)}\n")
                 
         except ValueError as e:
             print(f"\n{rule(100)}")
@@ -287,51 +290,42 @@ def main():
             print(f"Error: {e}")
             print(f"\nUse --list to see available categories")
             print(f"{rule(100)}\n")
-        except Exception as e:
-            print(f"\n{rule(100)}")
-            print(f"⚠️  DOWNLOAD ERROR")
-            print(f"{rule(100)}")
-            print(f"Error: {e}")
-            print(f"{rule(100)}\n")
+            raise
     
     elif args.list_downloads:
         # List downloaded categories
-        try:
-            downloaded = list_downloaded_pairs()
-            
-            if not downloaded:
-                print(f"\nNo downloaded VNNLIB categories found.")
-                print(f"Use --download <category> to download a benchmark.")
-                return
-            
-            # Group by category
-            by_category = {}
-            for pair in downloaded:
-                cat = pair['category']
-                if cat not in by_category:
-                    by_category[cat] = []
-                by_category[cat].append(pair)
-            
-            print(f"\n{rule(100)}")
-            print(f"DOWNLOADED VNNLIB CATEGORIES ({len(by_category)})")
-            print(f"{rule(100)}")
-            
-            for category in sorted(by_category.keys()):
-                instances = by_category[category]
-                info = CATEGORY_MAPPING.get(category, {})
-                
-                print(f"\n{category} ({len(instances)} instances)")
-                if info:
-                    print(f"  Type: {info.get('type', 'N/A')}")
-                    print(f"  Description: {info.get('description', 'N/A')}")
-                print(f"  Path: {instances[0]['category_path']}")
-            
-            print(f"\n{rule(100)}")
-            print(f"Total instances: {len(downloaded)}")
-            print(f"{rule(100)}\n")
+        downloaded = list_downloaded_pairs()
+        
+        if not downloaded:
+            print(f"\nNo downloaded VNNLIB categories found.")
+            print(f"Use --download <category> to download a benchmark.")
+            return
+        
+        # Group by category
+        by_category = {}
+        for pair in downloaded:
+            cat = pair['category']
+            if cat not in by_category:
+                by_category[cat] = []
+            by_category[cat].append(pair)
+        
+        print(f"\n{rule(100)}")
+        print(f"DOWNLOADED VNNLIB CATEGORIES ({len(by_category)})")
+        print(f"{rule(100)}")
+        
+        for category in sorted(by_category.keys()):
+            instances = by_category[category]
+            info = CATEGORY_MAPPING.get(category, {})
             
-        except Exception as e:
-            print(f"Error listing downloads: {e}")
+            print(f"\n{category} ({len(instances)} instances)")
+            if info:
+                print(f"  Type: {info.get('type', 'N/A')}")
+                print(f"  Description: {info.get('description', 'N/A')}")
+            print(f"  Path: {instances[0]['category_path']}")
+        
+        print(f"\n{rule(100)}")
+        print(f"Total instances: {len(downloaded)}")
+        print(f"{rule(100)}\n")
     
     else:
         parser.print_help()
diff --git a/act/front_end/vnnlib_loader/create_specs.py b/act/front_end/vnnlib_loader/create_specs.py
index 4abdf8bfe..9c7cd3b12 100644
--- a/act/front_end/vnnlib_loader/create_specs.py
+++ b/act/front_end/vnnlib_loader/create_specs.py
@@ -14,7 +14,7 @@
 
 from __future__ import annotations
 from pathlib import Path
-from typing import Any, List, Tuple, Dict, Optional
+from typing import Any, List, Tuple, Dict, Optional, override
 import logging
 import torch.nn as nn
 
@@ -57,7 +57,7 @@ class VNNLibSpecCreator(BaseSpecCreator):
     def __init__(
         self,
         config_name: Optional[str] = "vnnlib_default",
-        config_dict: Optional[Dict] = None
+        config_dict: Optional[Dict[str, Any]] = None
     ):
         """
         Initialize VNNLIB spec creator.
@@ -68,6 +68,7 @@ def __init__(
         """
         super().__init__(config_name, config_dict)
         
+    @override
     def create_specs_for_data_model_pairs(
         self,
         categories: Optional[List[str]] = None,
@@ -159,6 +160,7 @@ def create_specs_for_data_model_pairs(
         # different run.
         _onnx_cache: Dict[Tuple[str, str, Optional[str]], Dict[str, Any]] = {}
         
+        failures: List[str] = []
         for instance_info in all_instances:
             category = instance_info['category']
             onnx_model = instance_info['onnx_model']
@@ -193,14 +195,21 @@ def create_specs_for_data_model_pairs(
                     validate_shapes=validate_shapes
                 )
                 
-                if result is not None:
-                    results.append(result)
+                results.append(result)
                 
-            except Exception as e:
+            except UnsupportedSpecError:
+                raise
+            except Exception as e:  # noqa: BLE001 — collect every failure, raise below
                 logger.error(
                     f"Failed to create specs for {category}/{instance_id}: {e}"
                 )
+                failures.append(f"{category}/{instance_id}: {e}")
         
+        if failures:
+            raise RuntimeError(
+                f"Spec creation failed for {len(failures)}/{len(all_instances)} VNNLIB instance(s):\n  "
+                + "\n  ".join(failures)
+            )
         logger.info(f"Successfully created specs for {len(results)} instances")
         return results
     
@@ -208,15 +217,14 @@ def _create_specs_for_single_instance(
         self,
         category: str,
         instance_id: str,
-        instance_data: Dict,
+        instance_data: Dict[str, Any],
         validate_shapes: bool
-    ) -> Optional[Tuple[str, str, nn.Module, List[LabeledInputTensor], List[Tuple[InputSpec, OutputSpec]]]]:
+    ) -> Tuple[str, str, nn.Module, List[LabeledInputTensor], List[Tuple[InputSpec, OutputSpec]]]:
         """
         Create specs for a single VNNLIB instance.
         
         Returns:
             Tuple of (category, instance_id, pytorch_model, labeled_tensors, spec_pairs)
-            or None if failed
         """
         logger.info(f"Generating specs for {category}/{instance_id}")
         
@@ -227,23 +235,16 @@ def _create_specs_for_single_instance(
         # Parse VNNLIB to create specs
         # Pass input_shape to ensure specs match tensor shape (not flattened)
         # Pass true_label to promote RANGE to TOP1_ROBUST for classification
-        try:
-            queries = parse_vnnlib_queries(
-                vnnlib_path,
-                labeled_tensor=labeled_tensor,
-            )
-            if not queries:
-                raise RuntimeError("parse_vnnlib_queries returned no queries")
-            logger.info(
-                f"Parsed VNNLIB specs: {len(queries)} queries, "
-                f"first kind=({queries[0][0].kind}, {queries[0][1].kind})"
-            )
-        except UnsupportedSpecError as e:
-            logger.warning("UNSUPPORTED spec %s: %s", instance_id, e)
-            return None
-        except Exception as e:
-            logger.error(f"Failed to parse VNNLIB specs: {e}")
-            return None
+        queries = parse_vnnlib_queries(
+            vnnlib_path,
+            labeled_tensor=labeled_tensor,
+        )
+        if not queries:
+            raise RuntimeError(f"parse_vnnlib_queries returned no queries for {vnnlib_path}")
+        logger.info(
+            f"Parsed VNNLIB specs: {len(queries)} queries, "
+            f"first kind=({queries[0][0].kind}, {queries[0][1].kind})"
+        )
         
         spec_pairs = list(queries)
         
@@ -256,8 +257,9 @@ def _create_specs_for_single_instance(
             )
             
             if not validated_pairs:
-                logger.warning(f"Spec validation failed for {category}/{instance_id}")
-                return None
+                raise RuntimeError(
+                    f"No spec pair of {category}/{instance_id} matches the model's I/O shapes"
+                )
             
             spec_pairs = validated_pairs
         
@@ -318,6 +320,4 @@ def create_specs_from_paths(onnx_path, vnnlib_path, category: str = "custom"):
     }
     sr = VNNLibSpecCreator()._create_specs_for_single_instance(
         category, f"{onnx_p.stem}__{vnnlib_p.stem}", instance_data, validate_shapes=True)
-    if sr is None:
-        raise SystemExit(f"Spec creation failed (unsupported/invalid spec) for {vnnlib_p.name}")
     return sr
diff --git a/act/front_end/vnnlib_loader/data_model_loader.py b/act/front_end/vnnlib_loader/data_model_loader.py
index 411356cfa..02008003b 100644
--- a/act/front_end/vnnlib_loader/data_model_loader.py
+++ b/act/front_end/vnnlib_loader/data_model_loader.py
@@ -181,121 +181,112 @@ def download_vnnlib_category(
             'message': f"Failed to download instances.csv from all sources. Tried {len(VNNCOMP_REPO_URLS)} repositories."
         }
     
-    try:
-        # Parse instances.csv to get ONNX and VNNLIB files
-        instances: List[Dict[str, Any]] = []
-        onnx_files: set[str] = set()
-        vnnlib_files: set[str] = set()
-        with open(instances_file, 'r') as f:
-            reader = csv.reader(f)
-            rows = list(reader)
-            if rows and len(rows[0]) >= 2 and rows[0][0].strip().lower() == 'onnx':
-                rows = rows[1:]
-            
-            for row in rows:
-                if len(row) >= 3:
-                    onnx_field, vnnlib_field, timeout = row[0], row[1], row[2]
-                    onnx_entries = _parse_onnx_field(onnx_field)
-                    vnnlib_file = _normalize_rel_path(vnnlib_field)
-                    for _, onnx_file in onnx_entries:
-                        onnx_files.add(onnx_file)
-                    vnnlib_files.add(vnnlib_file)
-                    instances.append({
-                        'onnx': onnx_entries,
-                        'vnnlib': vnnlib_file,
-                        'timeout': timeout
-                    })
+    # Parse instances.csv to get ONNX and VNNLIB files
+    instances: List[Dict[str, Any]] = []
+    onnx_files: set[str] = set()
+    vnnlib_files: set[str] = set()
+    with open(instances_file, 'r') as f:
+        reader = csv.reader(f)
+        rows = list(reader)
+        if rows and len(rows[0]) >= 2 and rows[0][0].strip().lower() == 'onnx':
+            rows = rows[1:]
         
-        logger.info(f"Found {len(instances)} instances in category '{category}'")
+        for row in rows:
+            if len(row) >= 3:
+                onnx_field, vnnlib_field, timeout = row[0], row[1], row[2]
+                onnx_entries = _parse_onnx_field(onnx_field)
+                vnnlib_file = _normalize_rel_path(vnnlib_field)
+                for _, onnx_file in onnx_entries:
+                    onnx_files.add(onnx_file)
+                vnnlib_files.add(vnnlib_file)
+                instances.append({
+                    'onnx': onnx_entries,
+                    'vnnlib': vnnlib_file,
+                    'timeout': timeout
+                })
+    
+    logger.info(f"Found {len(instances)} instances in category '{category}'")
+    
+    # Download ONNX and VNNLIB files using the successful base URL
+    downloaded_onnx: set[str] = set()
+    downloaded_vnnlib: set[str] = set()
+    all_files: List[Tuple[str, set[str]]] = [(rel_path, downloaded_onnx) for rel_path in sorted(onnx_files)]
+    all_files.extend((rel_path, downloaded_vnnlib) for rel_path in sorted(vnnlib_files))
+    
+    for idx, (rel_path, downloaded_set) in enumerate(all_files, 1):
+        target_path = category_dir / rel_path
+        target_path.parent.mkdir(parents=True, exist_ok=True)
         
-        # Download ONNX and VNNLIB files using the successful base URL
-        downloaded_onnx: set[str] = set()
-        downloaded_vnnlib: set[str] = set()
-        all_files: List[Tuple[str, set[str]]] = [(rel_path, downloaded_onnx) for rel_path in sorted(onnx_files)]
-        all_files.extend((rel_path, downloaded_vnnlib) for rel_path in sorted(vnnlib_files))
+        # Try compressed first, then uncompressed.
+        tried_urls = []
+        success = False
         
-        for idx, (rel_path, downloaded_set) in enumerate(all_files, 1):
-            target_path = category_dir / rel_path
-            target_path.parent.mkdir(parents=True, exist_ok=True)
-            
-            # Try compressed first, then uncompressed.
-            tried_urls = []
-            success = False
+        for extension in ['.gz', '']:
+            file_url = f"{successful_base_url}/{repo_prefix}/{rel_path}{extension}"
+            tried_urls.append(file_url)
             
-            for extension in ['.gz', '']:
-                file_url = f"{successful_base_url}/{repo_prefix}/{rel_path}{extension}"
-                tried_urls.append(file_url)
+            try:
+                logger.debug(f"[{idx}/{len(all_files)}] Trying {rel_path}{extension}")
                 
-                try:
-                    logger.debug(f"[{idx}/{len(all_files)}] Trying {rel_path}{extension}")
+                if extension == '.gz':
+                    # Download compressed file
+                    gz_path = target_path.parent / f"{target_path.name}.gz"
+                    urllib.request.urlretrieve(file_url, gz_path)
                     
-                    if extension == '.gz':
-                        # Download compressed file
-                        gz_path = target_path.parent / f"{target_path.name}.gz"
-                        urllib.request.urlretrieve(file_url, gz_path)
-                        
-                        # Decompress
-                        with gzip.open(gz_path, 'rb') as f_in:
-                            with open(target_path, 'wb') as f_out:
-                                shutil.copyfileobj(f_in, f_out)
-                        
-                        # Remove .gz file
-                        gz_path.unlink()
-                        logger.debug(f"  ✓ Decompressed {rel_path}")
-                    else:
-                        # Download uncompressed file
-                        urllib.request.urlretrieve(file_url, target_path)
+                    # Decompress
+                    with gzip.open(gz_path, 'rb') as f_in:
+                        with open(target_path, 'wb') as f_out:
+                            shutil.copyfileobj(f_in, f_out)
                     
-                    downloaded_set.add(rel_path)
-                    success = True
-                    break
-                except Exception as e:
-                    logger.debug(f"  Failed with {extension}: {e}")
-                    continue
-            
-            if not success:
-                logger.warning(f"Failed to download {rel_path} from any URL")
-        
-        # Create metadata
-        metadata = {
-            'category': category,
-            'repo_name': repo_name,
-            'version': version,
-            'num_instances': len(instances),
-            'num_onnx_models': len(downloaded_onnx),
-            'num_vnnlib_specs': len(downloaded_vnnlib),
-            'source': successful_base_url,
-            'paths': {
-                'onnx': str(onnx_dir),
-                'vnnlib': str(vnnlib_dir),
-                'instances': str(instances_file)
-            }
-        }
-        
-        # Save metadata
-        metadata_path = category_dir / "info.json"
-        with open(metadata_path, 'w') as f:
-            json.dump(metadata, f, indent=2)
-        
-        logger.info(
-            f"Successfully downloaded category '{category}': "
-            f"{len(instances)} instances, {len(downloaded_onnx)} ONNX models, "
-            f"{len(downloaded_vnnlib)} VNNLIB specs"
-        )
-        
-        return {
-            'status': 'success',
-            'message': f"Downloaded {len(instances)} instances",
-            'category_path': str(category_dir),
-            'num_instances': len(instances)
-        }
+                    # Remove .gz file
+                    gz_path.unlink()
+                    logger.debug(f"  ✓ Decompressed {rel_path}")
+                else:
+                    # Download uncompressed file
+                    urllib.request.urlretrieve(file_url, target_path)
+                
+                downloaded_set.add(rel_path)
+                success = True
+                break
+            except Exception as e:
+                logger.debug(f"  Failed with {extension}: {e}")
+                continue
         
-    except Exception as e:
-        logger.error(f"Failed to download category '{category}': {e}")
-        return {
-            'status': 'error',
-            'message': str(e)
+        assert success, f"Failed to download {rel_path} from any of {tried_urls}"
+    
+    # Create metadata
+    metadata = {
+        'category': category,
+        'repo_name': repo_name,
+        'version': version,
+        'num_instances': len(instances),
+        'num_onnx_models': len(downloaded_onnx),
+        'num_vnnlib_specs': len(downloaded_vnnlib),
+        'source': successful_base_url,
+        'paths': {
+            'onnx': str(onnx_dir),
+            'vnnlib': str(vnnlib_dir),
+            'instances': str(instances_file)
         }
+    }
+    
+    # Save metadata
+    metadata_path = category_dir / "info.json"
+    with open(metadata_path, 'w') as f:
+        json.dump(metadata, f, indent=2)
+    
+    logger.info(
+        f"Successfully downloaded category '{category}': "
+        f"{len(instances)} instances, {len(downloaded_onnx)} ONNX models, "
+        f"{len(downloaded_vnnlib)} VNNLIB specs"
+    )
+    
+    return {
+        'status': 'success',
+        'message': f"Downloaded {len(instances)} instances",
+        'category_path': str(category_dir),
+        'num_instances': len(instances)
+    }
 
 
 def list_downloaded_pairs(root_dir: Optional[str] = None) -> List[Dict[str, Any]]:
@@ -338,44 +329,40 @@ def list_downloaded_pairs(root_dir: Optional[str] = None) -> List[Dict[str, Any]
         if not instances_file.exists():
             continue
         
-        try:
-            with open(instances_file, 'r') as f:
-                reader = csv.reader(f)
-                rows = list(reader)
-                if rows and len(rows[0]) >= 2 and rows[0][0].strip().lower() == 'onnx':
-                    rows = rows[1:]
-                
-                for row in rows:
-                    if len(row) >= 3:
-                        onnx_field, vnnlib_file, timeout = row[0], row[1], row[2]
-                        onnx_entries = _parse_onnx_field(onnx_field)
-                        vnnlib_rel = _normalize_rel_path(vnnlib_file)
-                        
-                        onnx_paths = [category_dir / onnx_rel for _, onnx_rel in onnx_entries]
-                        vnnlib_path = category_dir / vnnlib_rel
+        with open(instances_file, 'r') as f:
+            reader = csv.reader(f)
+            rows = list(reader)
+            if rows and len(rows[0]) >= 2 and rows[0][0].strip().lower() == 'onnx':
+                rows = rows[1:]
+            
+            for row in rows:
+                if len(row) >= 3:
+                    onnx_field, vnnlib_file, timeout = row[0], row[1], row[2]
+                    onnx_entries = _parse_onnx_field(onnx_field)
+                    vnnlib_rel = _normalize_rel_path(vnnlib_file)
+                    
+                    onnx_paths = [category_dir / onnx_rel for _, onnx_rel in onnx_entries]
+                    vnnlib_path = category_dir / vnnlib_rel
+                    
+                    # Only include if all referenced files exist
+                    if all(onnx_path.exists() for onnx_path in onnx_paths) and vnnlib_path.exists():
+                        first_onnx_rel = onnx_entries[0][1]
+                        paths: Dict[str, Any] = {
+                            'onnx': str(onnx_paths[0]),
+                            'vnnlib': str(vnnlib_path)
+                        }
+                        if len(onnx_entries) > 1:
+                            paths['onnx_models'] = [str(onnx_path) for onnx_path in onnx_paths]
                         
-                        # Only include if all referenced files exist
-                        if all(onnx_path.exists() for onnx_path in onnx_paths) and vnnlib_path.exists():
-                            first_onnx_rel = onnx_entries[0][1]
-                            paths: Dict[str, Any] = {
-                                'onnx': str(onnx_paths[0]),
-                                'vnnlib': str(vnnlib_path)
-                            }
-                            if len(onnx_entries) > 1:
-                                paths['onnx_models'] = [str(onnx_path) for onnx_path in onnx_paths]
-                            
-                            all_instances.append({
-                                'category': category_dir.name,
-                                'onnx_model': first_onnx_rel,
-                                'onnx_models': onnx_entries,
-                                'vnnlib_spec': vnnlib_rel,
-                                'timeout': float(timeout) if timeout else None,
-                                'is_dual_model': len(onnx_entries) > 1,
-                                'paths': paths
-                            })
-        
-        except Exception as e:
-            logger.warning(f"Failed to read instances from {category_dir.name}: {e}")
+                        all_instances.append({
+                            'category': category_dir.name,
+                            'onnx_model': first_onnx_rel,
+                            'onnx_models': onnx_entries,
+                            'vnnlib_spec': vnnlib_rel,
+                            'timeout': float(timeout) if timeout else None,
+                            'is_dual_model': len(onnx_entries) > 1,
+                            'paths': paths
+                        })
     
     return all_instances
 
@@ -670,62 +657,49 @@ def model_inference_with_vnnlib(
     model_name = Path(onnx_model).stem
     combo_id = f"{category}+{model_name}"
     
-    try:
-        # Load the pair
+    # Load the pair
+    if verbose:
+        logger.info(f"Testing: {category} + {model_name}")
+    
+    result = load_vnnlib_pair(
+        category=category,
+        onnx_model=onnx_model,
+        vnnlib_spec=vnnlib_spec,
+        root_dir=root_dir,
+        auto_download=True
+    )
+    
+    model = result['model']
+    labeled_tensor = result['labeled_tensor']
+    input_tensor = labeled_tensor.tensor  # Already has batch dimension
+    
+    # Run inference
+    success, output, error_msg = infer_single_model(
+        combo_id, 
+        model, 
+        input_tensor  # Already (1, C, H, W)
+    )
+    
+    if success:
+        if output is None:
+            raise RuntimeError("Inference succeeded without an output tensor")
         if verbose:
-            logger.info(f"Testing: {category} + {model_name}")
-        
-        result = load_vnnlib_pair(
-            category=category,
-            onnx_model=onnx_model,
-            vnnlib_spec=vnnlib_spec,
-            root_dir=root_dir,
-            auto_download=True
-        )
-        
-        model = result['model']
-        labeled_tensor = result['labeled_tensor']
-        input_tensor = labeled_tensor.tensor  # Already has batch dimension
-        
-        # Run inference
-        success, output, error_msg = infer_single_model(
-            combo_id, 
-            model, 
-            input_tensor  # Already (1, C, H, W)
-        )
-        
-        if success:
-            if output is None:
-                raise RuntimeError("Inference succeeded without an output tensor")
-            if verbose:
-                logger.info(f"  ✓ SUCCESS - Output shape: {output.shape}")
-            return {
-                'category': category,
-                'model': model_name,
-                'spec': vnnlib_spec,
-                'status': 'success',
-                'output_shape': tuple(output.shape)
-            }
-        else:
-            if verbose:
-                logger.warning(f"  ✗ FAILED - {error_msg}")
-            return {
-                'category': category,
-                'model': model_name,
-                'spec': vnnlib_spec,
-                'status': 'failed',
-                'error': error_msg
-            }
-            
-    except Exception as e:
-        error_msg = str(e)[:100]
+            logger.info(f"  ✓ SUCCESS - Output shape: {output.shape}")
+        return {
+            'category': category,
+            'model': model_name,
+            'spec': vnnlib_spec,
+            'status': 'success',
+            'output_shape': tuple(output.shape)
+        }
+    else:
         if verbose:
-            logger.error(f"  ✗ ERROR - {error_msg}")
+            logger.warning(f"  ✗ FAILED - {error_msg}")
         return {
             'category': category,
             'model': model_name,
             'spec': vnnlib_spec,
-            'status': 'error',
+            'status': 'failed',
             'error': error_msg
         }
 
@@ -804,9 +778,5 @@ def get_category_info(category: str, root_dir: Optional[str] = None) -> Optional
     if not info_path.exists():
         return None
     
-    try:
-        with open(info_path, 'r') as f:
-            return json.load(f)
-    except Exception as e:
-        logger.error(f"Failed to read category info: {e}")
-        return None
+    with open(info_path, 'r') as f:
+        return json.load(f)
diff --git a/act/front_end/vnnlib_loader/onnx_converter.py b/act/front_end/vnnlib_loader/onnx_converter.py
index aba299106..2d6a530ca 100644
--- a/act/front_end/vnnlib_loader/onnx_converter.py
+++ b/act/front_end/vnnlib_loader/onnx_converter.py
@@ -14,7 +14,7 @@
 
 from __future__ import annotations
 from pathlib import Path
-from typing import Tuple, Optional
+from typing import Tuple
 import logging
 import torch
 import torch.nn as nn
@@ -458,46 +458,41 @@ def get_onnx_metadata(onnx_path: Path) -> dict:
     Returns:
         Dict with model metadata (producer, version, shapes, etc.)
     """
-    try:
-        import onnx
-        
-        onnx_model = onnx.load(str(onnx_path))
-        
-        metadata = {
-            'producer_name': onnx_model.producer_name,
-            'producer_version': onnx_model.producer_version,
-            'ir_version': onnx_model.ir_version,
-            'opset_version': None,
-            'input_shapes': [],
-            'output_shapes': []
-        }
-        
-        # Get opset version
-        if onnx_model.opset_import:
-            metadata['opset_version'] = onnx_model.opset_import[0].version
-        
-        # Get input/output shapes
-        graph = onnx_model.graph
-        
-        for inp in graph.input:
-            shape = _extract_shape_from_tensor(inp)
-            metadata['input_shapes'].append({
-                'name': inp.name,
-                'shape': shape
-            })
-        
-        for out in graph.output:
-            shape = _extract_shape_from_tensor(out)
-            metadata['output_shapes'].append({
-                'name': out.name,
-                'shape': shape
-            })
-        
-        return metadata
-        
-    except Exception as e:
-        logger.error(f"Failed to extract ONNX metadata: {e}")
-        return {}
+    import onnx
+    
+    onnx_model = onnx.load(str(onnx_path))
+    
+    metadata = {
+        'producer_name': onnx_model.producer_name,
+        'producer_version': onnx_model.producer_version,
+        'ir_version': onnx_model.ir_version,
+        'opset_version': None,
+        'input_shapes': [],
+        'output_shapes': []
+    }
+    
+    # Get opset version
+    if onnx_model.opset_import:
+        metadata['opset_version'] = onnx_model.opset_import[0].version
+    
+    # Get input/output shapes
+    graph = onnx_model.graph
+    
+    for inp in graph.input:
+        shape = _extract_shape_from_tensor(inp)
+        metadata['input_shapes'].append({
+            'name': inp.name,
+            'shape': shape
+        })
+    
+    for out in graph.output:
+        shape = _extract_shape_from_tensor(out)
+        metadata['output_shapes'].append({
+            'name': out.name,
+            'shape': shape
+        })
+    
+    return metadata
 
 
 def validate_onnx_file(onnx_path: Path) -> bool:
@@ -508,53 +503,18 @@ def validate_onnx_file(onnx_path: Path) -> bool:
         onnx_path: Path to .onnx file
         
     Returns:
-        True if valid, False otherwise
+        True if the model passes the ONNX checker, False if it is malformed.
+        Load errors (missing file, unreadable protobuf) are raised.
     """
+    import onnx
+    
+    onnx_model = onnx.load(str(onnx_path))
     try:
-        import onnx
-        
-        onnx_model = onnx.load(str(onnx_path))
         onnx.checker.check_model(onnx_model)
-        logger.info(f"ONNX model validated: {onnx_path.name}")
-        return True
-        
-    except Exception as e:
-        logger.error(f"ONNX validation failed: {e}")
+    except onnx.checker.ValidationError as e:
+        logger.warning(f"ONNX validation failed for {onnx_path.name}: {e}")
         return False
+    logger.info(f"ONNX model validated: {onnx_path.name}")
+    return True
 
 
-def convert_and_save_pytorch(
-    onnx_path: Path,
-    output_path: Optional[Path] = None,
-    simplify: bool = True
-) -> Path:
-    """
-    Convert ONNX model to PyTorch and save as .pt file.
-    
-    Args:
-        onnx_path: Path to .onnx file
-        output_path: Path for .pt file (defaults to same dir as ONNX)
-        simplify: Whether to simplify ONNX before conversion
-        
-    Returns:
-        Path to saved .pt file
-        
-    Raises:
-        ONNXConversionError: If conversion or saving fails
-    """
-    try:
-        # Convert to PyTorch
-        pytorch_model = convert_onnx_to_pytorch(onnx_path, simplify=simplify)
-        
-        # Determine output path
-        if output_path is None:
-            output_path = onnx_path.with_suffix('.pt')
-        
-        # Save model
-        torch.save(pytorch_model.state_dict(), output_path)
-        logger.info(f"Saved PyTorch model to {output_path}")
-        
-        return output_path
-        
-    except Exception as e:
-        raise ONNXConversionError(f"Failed to convert and save: {str(e)}")
diff --git a/act/front_end/vnnlib_loader/vnnlib_parser.py b/act/front_end/vnnlib_loader/vnnlib_parser.py
index b7f39abc6..34f21e860 100644
--- a/act/front_end/vnnlib_loader/vnnlib_parser.py
+++ b/act/front_end/vnnlib_loader/vnnlib_parser.py
@@ -32,11 +32,89 @@ class VNNLibParseError(Exception):
     pass
 
 
-class UnsupportedSpecError(Exception):
+class UnsupportedSpecError(ValueError):
     """Exception raised for soundly unsupported VNNLIB features."""
     pass
 
 
+_DECLARE_NETWORK_RE = re.compile(r"\(\s*declare-network\s+([A-Za-z_]\w*)\b")
+_DECLARE_INPUT_RE = re.compile(
+    r"\(\s*declare-input\s+([A-Za-z_]\w*)\s+\S+\s+\[([^\]]+)\]\s*\)",
+    re.MULTILINE,
+)
+_ASSERT_RE = re.compile(r"\(\s*assert\b")
+
+
+def _declaration_prefix(vnnlib_path: Path) -> str:
+    """Read only the declarations preceding the first VNNLIB assertion."""
+    lines: List[str] = []
+    try:
+        with open(vnnlib_path, "r") as source:
+            for line in source:
+                assert_match = _ASSERT_RE.search(line)
+                lines.append(line if assert_match is None else line[:assert_match.start()])
+                if assert_match is not None:
+                    break
+    except OSError as exc:
+        raise VNNLibParseError(f"Failed to read {vnnlib_path}: {exc}") from exc
+    return "".join(lines)
+
+
+def _network_declaration_blocks(prefix: str) -> List[Tuple[str, str]]:
+    """Return complete ``declare-network`` forms from a declaration prefix."""
+    uncommented = re.sub(r";[^\n]*", "", prefix)
+    blocks: List[Tuple[str, str]] = []
+    for match in _DECLARE_NETWORK_RE.finditer(uncommented):
+        depth = 0
+        for index in range(match.start(), len(uncommented)):
+            char = uncommented[index]
+            if char == "(":
+                depth += 1
+            elif char == ")":
+                depth -= 1
+                if depth == 0:
+                    blocks.append((match.group(1), uncommented[match.start():index + 1]))
+                    break
+    return blocks
+
+
+def reject_multi_input_vnnlib(vnnlib_path: Path) -> None:
+    """Reject VNNLIB 2.0 networks declaring multiple input tensors.
+
+    The scan stops at the first assertion, so even very large properties are
+    rejected without tokenizing or constructing their assertion AST. Separate
+    one-input ``declare-network`` blocks remain supported for isomorphic specs.
+    Legacy VNNLIB 1.0 ``declare-const X_i`` declarations denote one flat input
+    tensor and therefore do not trigger this check.
+    """
+    prefix = _declaration_prefix(vnnlib_path)
+    network_blocks = _network_declaration_blocks(prefix)
+    if not network_blocks:
+        network_blocks = [("<unnamed>", prefix)]
+
+    for network_name, block in network_blocks:
+        declarations = []
+        for match in _DECLARE_INPUT_RE.finditer(block):
+            raw_shape = match.group(2)
+            try:
+                shape = tuple(int(part.strip()) for part in raw_shape.split(",") if part.strip())
+            except ValueError as exc:
+                raise VNNLibParseError(
+                    f"Invalid VNNLIB 2.0 declare-input shape: {raw_shape}"
+                ) from exc
+            declarations.append((match.group(1), shape))
+
+        if len(declarations) > 1:
+            rendered = ", ".join(
+                f"{name} [{', '.join(str(dim) for dim in shape)}]"
+                for name, shape in declarations
+            )
+            raise UnsupportedSpecError(
+                f"{vnnlib_path}: multiple input tensors are unsupported; "
+                f"network {network_name!r} declares {len(declarations)} inputs: {rendered}"
+            )
+
+
 # -------------------------------------------------------------------------
 # Public API
 # -------------------------------------------------------------------------
@@ -67,6 +145,8 @@ def parse_vnnlib_to_tensors(
     """
     if not vnnlib_path.exists():
         raise VNNLibParseError(f"VNNLIB file not found: {vnnlib_path}")
+
+    reject_multi_input_vnnlib(vnnlib_path)
     
     try:
         with open(vnnlib_path, 'r') as f:
@@ -96,15 +176,12 @@ def parse_vnnlib_to_tensors(
         # Constraints inside (or ...) branches must not be intersected here —
         # that would produce empty boxes for disjunctive-input properties
         # (e.g. ACAS Xu prop_5..10).
-        try:
-            forms = _parse_all_forms(content)
-            simple_bodies = [
-                f[1] for f in forms
-                if isinstance(f, list) and len(f) >= 2 and f[0] == "assert"
-                and _is_simple_x_bound(f[1])
-            ]
-        except Exception:
-            simple_bodies = []
+        forms = _parse_all_forms(content)
+        simple_bodies = [
+            f[1] for f in forms
+            if isinstance(f, list) and len(f) >= 2 and f[0] == "assert"
+            and _is_simple_x_bound(f[1])
+        ]
         input_bounds = _extract_input_bounds(simple_bodies, num_inputs)
         
         # Create input tensor from bounds center
@@ -238,23 +315,19 @@ def extract_label_from_vnnlib(vnnlib_path: Path) -> Optional[int]:
         >>> print(label)
         14
     """
-    try:
-        with open(vnnlib_path, 'r') as f:
-            # Read first few lines (label is typically in first comment)
-            for _ in range(5):
-                line = f.readline()
-                if not line:
-                    break
-                
-                # Match patterns like: ; CIFAR100 property with label: 14.
-                match = re.search(r'label:\s*(\d+)', line, re.IGNORECASE)
-                if match:
-                    return int(match.group(1))
-        
-        return None
-    except Exception as e:
-        logger.debug(f"Failed to extract label from {vnnlib_path}: {e}")
-        return None
+    with open(vnnlib_path, 'r') as f:
+        # Read first few lines (label is typically in first comment)
+        for _ in range(5):
+            line = f.readline()
+            if not line:
+                break
+            
+            # Match patterns like: ; CIFAR100 property with label: 14.
+            match = re.search(r'label:\s*(\d+)', line, re.IGNORECASE)
+            if match:
+                return int(match.group(1))
+    
+    return None
 
 
 # -------------------------------------------------------------------------
@@ -280,6 +353,7 @@ def parse_vnnlib_2_0(
     """Parse VNNLIB 2.0 by ravel-rewriting bracket variables to legacy names."""
     if not vnnlib_path.exists():
         raise VNNLibParseError(f"VNNLIB file not found: {vnnlib_path}")
+    reject_multi_input_vnnlib(vnnlib_path)
     try:
         with open(vnnlib_path, 'r') as f:
             content = f.read()
@@ -597,16 +671,12 @@ def _extract_input_bounds(
             continue
         x_tok = left if x_is_left else right
         lit_tok = right if x_is_left else left
-        try:
-            val = float(lit_tok)
-        except (TypeError, ValueError):
-            continue
+        val = float(lit_tok)  # _is_simple_x_bound admitted only numeric literals
         x_match = _X_RE.fullmatch(x_tok)
         if x_match is None:
             continue
         idx = int(x_match.group(1))
-        if idx >= num_inputs:
-            continue
+        assert idx < num_inputs, f"X_{idx} is bounded but the property declares {num_inputs} inputs"
         # (<= X val)  -> X <= val   (upper)
         # (>= X val)  -> X >= val   (lower)
         # (<= val X)  -> val <= X   -> X >= val (lower)
diff --git a/act/pipeline/__init__.py b/act/pipeline/__init__.py
index 43a81b077..27298e302 100644
--- a/act/pipeline/__init__.py
+++ b/act/pipeline/__init__.py
@@ -22,7 +22,6 @@
     - ModelFactory: Create PyTorch models from YAML configurations
     - TorchToACT: Convert PyTorch models to ACT representation
     - VerifierValidator: Validate verifier correctness with concrete tests
-    - PerformanceProfiler: Profile execution time and memory usage
 
 All verification utilities are located in the verification/ submodule.
 
@@ -42,40 +41,8 @@
 from act.pipeline.verification.model_factory import ModelFactory
 from act.pipeline.verification.torch2act import TorchToACT
 
-# Import utilities
-try:
-    from act.pipeline.verification.utils import (
-        PerformanceProfiler,
-        ParallelExecutor,
-        print_memory_usage,
-        clear_torch_cache,
-        setup_logging,
-        ProgressTracker,
-    )
-    UTILS_AVAILABLE = True
-except ImportError:
-    UTILS_AVAILABLE = False
-    PerformanceProfiler = None
-    ParallelExecutor = None
-    print_memory_usage = None
-    clear_torch_cache = None
-    setup_logging = None
-    ProgressTracker = None
-
-
 __all__ = [
     # Core model factory and conversion
     'ModelFactory',
     'TorchToACT',
-    
-    # Utilities
-    'PerformanceProfiler',
-    'ParallelExecutor',
-    'print_memory_usage',
-    'clear_torch_cache',
-    'setup_logging',
-    'ProgressTracker',
-    
-    # Availability flags
-    'UTILS_AVAILABLE',
 ]
diff --git a/act/pipeline/fuzzing/actfuzzer.py b/act/pipeline/fuzzing/actfuzzer.py
index deca71594..547660801 100644
--- a/act/pipeline/fuzzing/actfuzzer.py
+++ b/act/pipeline/fuzzing/actfuzzer.py
@@ -549,16 +549,10 @@ def _generate_report(self) -> FuzzingReport:
         total_time = time.time() - self.start_time
 
         # Neurons that were never activated across all iterations
-        never_activated_neurons: List[Tuple[str, int]] = []
-        never_activated_count = 0
-        try:
-            uncovered = self.coverage_tracker.get_uncovered_neurons()
-            never_activated_count = len(uncovered)
-            # Deterministic small sample for logs/report
-            never_activated_neurons = sorted(list(uncovered))[:20]
-        except Exception:
-            never_activated_count = 0
-            never_activated_neurons = []
+        uncovered = self.coverage_tracker.get_uncovered_neurons()
+        never_activated_count = len(uncovered)
+        # Deterministic small sample for logs/report
+        never_activated_neurons: List[Tuple[str, int]] = sorted(list(uncovered))[:20]
 
         report = FuzzingReport(
             total_iterations=self.iterations,
diff --git a/act/pipeline/verification/model_factory.py b/act/pipeline/verification/model_factory.py
index 1cf65bc33..fe4a05e9c 100644
--- a/act/pipeline/verification/model_factory.py
+++ b/act/pipeline/verification/model_factory.py
@@ -67,10 +67,7 @@ def _discover_net_names(nets_dir: Path, manifest_path: Optional[Path]) -> List[s
                 break
 
     if manifest_path is not None and manifest_path.exists():
-        try:
-            names.extend(str(n) for n in _load_manifest(manifest_path))
-        except Exception as e:
-            logger.warning(f"Failed to read manifest {manifest_path}: {e}")
+        names.extend(str(n) for n in _load_manifest(manifest_path))
 
     names.extend(p.stem for p in sorted(nets_dir.glob('*.json')))
 
@@ -123,26 +120,25 @@ def _load_all_nets(self) -> None:
         - Enables O(1) lookup via get_act_net()
         - Costs ~10-20MB memory for typical test suites
         """
+        # Callers that only need VNNLIB/TorchVision models construct the factory
+        # before nets are generated; consumers that need nets check list_networks().
         if not self.nets_dir.exists():
-            logger.warning(f"Nets dir not found: {self.nets_dir}")
+            logger.debug(f"Nets dir not found: {self.nets_dir}")
             return
         
         for name in self.net_names:
             net_path = self.nets_dir / f"{name}.json"
             
             if not net_path.exists():
-                logger.warning(f"ACT Net file not found: {net_path}. Skipping '{name}'.")
-                continue
+                raise FileNotFoundError(
+                    f"ACT Net '{name}' is listed in the manifest but {net_path} does not exist"
+                )
             
-            try:
-                with open(net_path, 'r') as f:
-                    net_dict = json.load(f)
-                act_net = NetSerializer.deserialize_net(net_dict)
-                self.nets[name] = act_net
-                logger.debug(f"Pre-loaded ACT Net '{name}' from {net_path}")
-            except Exception as e:
-                logger.error(f"Failed to load ACT Net '{name}' from {net_path}: {e}")
-                continue
+            with open(net_path, 'r') as f:
+                net_dict = json.load(f)
+            act_net = NetSerializer.deserialize_net(net_dict)
+            self.nets[name] = act_net
+            logger.debug(f"Pre-loaded ACT Net '{name}' from {net_path}")
         
         logger.info(f"Pre-loaded {len(self.nets)} ACT Nets from {self.nets_dir}")
     
@@ -342,11 +338,17 @@ def main():
     print("PyTorch Model Factory - Spec-Free Verification Testing")
     print(rule())
     
-    all_passed = True
+    failures: List[str] = []
     total_tests = 0
     passed_tests = 0
     
-    for name in factory.list_networks():
+    network_names = factory.list_networks()
+    if not network_names:
+        raise RuntimeError(
+            f"No ACT Nets found in {factory.nets_dir}; run `python -m act.back_end --generate` first"
+        )
+    
+    for name in network_names:
         print(f"\n{rule()}")
         print(f"Network: {name}")
         print(rule())
@@ -395,13 +397,15 @@ def main():
                         
                         # Track test success
                         total_tests += 1
+                        # Constraint outcomes are properties of the (random-weight)
+                        # network on this input, not conversion errors.
                         if input_satisfied and output_satisfied:
                             passed_tests += 1
-                            print(f"  ✅ Test PASSED (both constraints satisfied)")
+                            print(f"  ✅ Both constraints satisfied")
                         elif not input_satisfied:
-                            print(f"  ⚠️  Test UNCERTAIN (input constraint violated)")
+                            print(f"  ℹ️  Input outside spec region (property not applicable)")
                         else:
-                            print(f"  ❌ Test FAILED (output constraint violated)")
+                            print(f"  ℹ️  Output property violated on this input (counterexample)")
                     
                     else:
                         # Legacy nn.Module (no verification)
@@ -415,35 +419,31 @@ def main():
                     print(f"  ❌ Test case '{test_case}' failed: {e}")
                     import traceback
                     traceback.print_exc()
-                    all_passed = False
+                    failures.append(f"{name}/{test_case}: {e}")
             
         except Exception as e:
             print(f"\n❌ Failed to create/test model '{name}': {e}")
             import traceback
             traceback.print_exc()
-            all_passed = False
+            failures.append(f"{name}: {e}")
     
     # Print summary
     print("\n" + rule())
     print(f"📊 Verification Test Summary:")
     print(f"   Total tests: {total_tests}")
-    print(f"   ✅ Passed: {passed_tests}")
-    print(f"   ⚠️  Uncertain/Failed: {total_tests - passed_tests}")
-    if total_tests > 0:
-        success_rate = (passed_tests / total_tests) * 100
-        print(f"   Success rate: {success_rate:.1f}%")
+    print(f"   ✅ Both constraints satisfied: {passed_tests}")
+    print(f"   ℹ️  Input outside spec / property violated: {total_tests - passed_tests}")
+    if total_tests == 0:
+        raise RuntimeError("No ACT→PyTorch test cases were executed")
     print(rule())
     
-    if all_passed:
-        print("✅ All models created and tested successfully")
-    else:
-        print("⚠️  Some models had issues - see details above")
+    if failures:
+        raise RuntimeError(
+            f"{len(failures)} ACT→PyTorch model/test-case error(s):\n  " + "\n  ".join(failures)
+        )
+    print("✅ All models created and tested successfully")
     print(rule())
 
-    if not all_passed:
-        import sys
-        sys.exit(1)
-
 
 if __name__ == "__main__":
     main()
diff --git a/act/pipeline/verification/torch2act.py b/act/pipeline/verification/torch2act.py
index 728ed0889..67b65fa89 100644
--- a/act/pipeline/verification/torch2act.py
+++ b/act/pipeline/verification/torch2act.py
@@ -69,7 +69,7 @@
 from act.back_end.layer_util import create_layer
 from act.back_end.utils import avgpool2d_output_hw
 from act.pipeline.verification.utils import (
-    _prod, _normalize_tuple, _assert_dag, _broadcast_const_to_size,
+    _prod, _normalize_tuple, _assert_dag, _assert_dataflow, _broadcast_const_to_size,
     _normalize_axes, _reduce_output_shape, _compute_slice_output_shape,
     ONNX_HANDLERS,
 )
@@ -77,8 +77,6 @@
 # Imports needed for main() test harness
 from act.util.model_inference import model_inference
 from act.front_end.model_synthesis import model_synthesis
-from act.back_end.solver.solver_torchlp import TorchLPSolver
-from act.back_end.solver.solver_gurobi import GurobiSolver
 from act.util.options import PerformanceOptions
 from act.util.format_utils import rule
 
@@ -148,6 +146,12 @@ def __init__(
         # would mis-wire them. _build_preds_succs honours this override.
         self._fx_pred_override: Dict[int, List[int]] = {}
 
+        # Head layer of each node converted into a chain of layers (BatchNorm
+        # -> SCALE + BIAS). node_to_layer_id maps a node to its LAST layer so
+        # successors read its output; incoming FX edges must enter the head,
+        # otherwise the layers in between are bypassed. See _record_chain_head.
+        self._node_first_layer_id: Dict[str, int] = {}
+
         # Compile-time constants (e.g. OnnxShape values) that must NOT enter
         # the runtime IR. Resolved by ``_resolve_constant_tensor`` BEFORE any
         # placeholder/sample_input fallback — this is what stops shape chains
@@ -898,11 +902,8 @@ def _evaluate_constant_subgraph(self, node_name: str) -> Optional[torch.Tensor]:
                 arg_vals.append(v)
             else:
                 arg_vals.append(a)
-        try:
-            with torch.no_grad():
-                return sub(*arg_vals)
-        except Exception:
-            return None
+        with torch.no_grad():
+            return sub(*arg_vals)
 
     def _ensure_constant_vars(self, node_name: str) -> bool:
         """Emit a CONSTANT layer for an ONNX initializer (consumed by Concat /
@@ -972,6 +973,7 @@ def _process_fx_graph(self) -> None:
         if self.fx_graph is None:
             return
         for node in self.fx_graph.nodes:
+            first_layer_id = len(self.layers)
             if node.op == 'placeholder':
                 pass  # Already pre-registered in _pre_register_nodes
             elif node.op == 'call_module':
@@ -984,6 +986,27 @@ def _process_fx_graph(self) -> None:
                 self._handle_get_attr(node)
             elif node.op == 'output':
                 self._handle_output(node)
+            self._record_chain_head(node.name, first_layer_id)
+    
+    def _record_chain_head(self, node_name: str, first_layer_id: int) -> None:
+        """Route a node's incoming FX edges to the head of the chain it emitted.
+
+        Only a contiguous chain of data layers ending at the node's registered
+        layer qualifies (BatchNorm SCALE -> BIAS, const - x, DequantizeLinear).
+        Other expansions keep the default wiring, e.g. sibling SLICEs of a
+        split (pinned via _fx_pred_override) or a CONSTANT emitted before its
+        consumer.
+        """
+        last = self.node_to_layer_id.get(node_name)
+        if last is None or last <= first_layer_id:
+            return
+        chain = range(first_layer_id, last + 1)
+        if not all(self.layers[lid].in_vars for lid in chain):
+            return
+        for prev, cur in zip(chain, chain[1:]):
+            if not set(self.layers[cur].in_vars) <= set(self.layers[prev].out_vars):
+                return
+        self._node_first_layer_id[node_name] = first_layer_id
     
     def _handle_call_module(self, node: fx.Node) -> None:
         """Handle call_module node."""
@@ -1007,6 +1030,10 @@ def _handle_call_module(self, node: fx.Node) -> None:
     
     def _handle_call_function(self, node: fx.Node) -> None:
         """Handle call_function node."""
+        if node.target is nn.functional.adaptive_avg_pool2d:
+            self._process_adaptive_avg_pool2d_function(node)
+            return
+        
         target_name = str(node.target).lower()
         
         handlers = {
@@ -1088,14 +1115,17 @@ def _build_preds_succs(self) -> Tuple[Dict[int, List[int]], Dict[int, List[int]]
         """Build preds and succs dictionaries, validating DAG property.
         
         Uses a hybrid approach:
-        1. Build edges from FX graph for mapped nodes
-        2. For unmapped intermediate layers (e.g., SCALE from BatchNorm), 
-           connect them sequentially based on layer creation order
+        1. Build edges from FX graph for mapped nodes; a node converted into
+           a chain of layers is entered at the chain head
+        2. Connect the remaining layers of a multi-layer conversion (e.g. BIAS
+           after BatchNorm's SCALE) sequentially by layer creation order
         """
         n_layers = len(self.layers)
         
-        # Identify which layers are mapped to FX nodes
+        # Identify which layers are mapped to FX nodes. The head of a chain
+        # conversion receives that node's incoming FX edges.
         mapped_layer_ids = set(lid for lid in self.node_to_layer_id.values() if lid >= 0)
+        mapped_layer_ids.update(self._node_first_layer_id.values())
         
         preds: Dict[int, List[int]] = {i: [] for i in range(n_layers)}
         succs: Dict[int, List[int]] = {i: [] for i in range(n_layers)}
@@ -1108,6 +1138,7 @@ def _build_preds_succs(self) -> Tuple[Dict[int, List[int]], Dict[int, List[int]]
             layer_id = self.node_to_layer_id.get(node_name)
             if layer_id is None or layer_id < 0:
                 continue
+            layer_id = self._node_first_layer_id.get(node_name, layer_id)
             
             for pred_name in pred_names:
                 pred_layer_id = self.node_to_layer_id.get(pred_name)
@@ -1122,8 +1153,8 @@ def _build_preds_succs(self) -> Tuple[Dict[int, List[int]], Dict[int, List[int]]
                 if pred_layer_id != layer_id and pred_layer_id not in preds[layer_id]:
                     preds[layer_id].append(pred_layer_id)
         
-        # Second, connect unmapped layers (SCALE, BIAS from BatchNorm, etc.) sequentially
-        # These layers are internal to a multi-layer conversion and should connect to i-1.
+        # Second, connect layers internal to a multi-layer conversion (e.g. BIAS
+        # after BatchNorm's SCALE) sequentially: they connect to i-1.
         # Source layers (``in_vars == []``, e.g. CONSTANT emitted by
         # ``_ensure_constant_vars``) are intentionally exempt -- they have no
         # data dependency on anything upstream, so wiring them to ``i-1`` would
@@ -1188,6 +1219,9 @@ def _convert_module(self, mod: nn.Module) -> None:
         if kind == LayerKind.RELU.value:
             self._convert_activation(mod, LayerKind.RELU)
             return
+        if kind == LayerKind.RELU6.value:
+            self._convert_activation(mod, LayerKind.RELU6)
+            return
         if kind == LayerKind.CONV2D.value and isinstance(mod, nn.Conv2d):
             self._convert_conv2d(mod)
             return
@@ -1904,6 +1938,14 @@ def _process_mul_operation(self, node: fx.Node) -> None:
                 self.shape = x_shape
                 self._register_node(node.name, layer_id)
     
+    def _process_adaptive_avg_pool2d_function(self, node: fx.Node) -> None:
+        """Process F.adaptive_avg_pool2d() via the nn.AdaptiveAvgPool2d converter."""
+        if not self._get_predecessor_state(node):
+            return
+        output_size = node.args[1] if len(node.args) > 1 else node.kwargs["output_size"]
+        self._convert_adaptive_avgpool2d(nn.AdaptiveAvgPool2d(output_size))
+        self._register_node(node.name)
+    
     def _process_mean_operation(self, node: fx.Node) -> None:
         """Process torch.mean()."""
         if not self._get_predecessor_state(node):
@@ -2076,6 +2118,7 @@ def run(self) -> Net:
         
         # Build and validate network
         preds, succs = self._build_layer_graph()
+        _assert_dataflow(self.layers, preds)
         net = Net(layers=self.layers, preds=preds, succs=succs)
         
         from act.back_end.layer_util import validate_graph
@@ -2223,7 +2266,7 @@ def _build_layer_graph(self) -> Tuple[Dict[int, List[int]], Dict[int, List[int]]
 # -----------------------------------------------------------------------------
 
 def main():
-    """Main entry point for PyTorch→ACT conversion and verification testing."""
+    """Main entry point for PyTorch→ACT conversion testing."""
     # Initialize debug file (GUARDED)
     if PerformanceOptions.debug_tf:
         debug_file = PerformanceOptions.debug_output_file
@@ -2245,61 +2288,22 @@ def main():
     print(f"  {len(successful_models)} models passed inference tests")
     
     if not successful_models:
-        print("  No successful models to verify!")
-        exit(1)
-    
-    # Step 3: Convert and verify all successful models (memory-efficient)
-    print(f"\n Step 3: Converting and verifying all {len(successful_models)} successful models...")
-    print(f"  Processing one at a time to avoid memory issues...")
+        raise RuntimeError("No synthesized model passed inference; nothing to convert")
     
-    # Import verification functions
-    from act.back_end.verifier import verify_once
+    # Step 3: Convert every successful model (one at a time to bound memory).
+    print(f"\n Step 3: Converting all {len(successful_models)} successful models...")
     
     import gc
     import torch as torch_module
     
-    conversion_results = {}
-    verification_results = {}
-    conversion_success_count = 0
-    verification_success_count = 0
-    
-    # Step 4: Initialize solvers (moved earlier to reuse for all models)
-    print("\n Step 4: Initializing solvers...")
-    gurobi_solver = None
-    torch_solver = None
-    
-    try:
-        gurobi_solver = GurobiSolver()
-        print("  Gurobi solver available")
-    except Exception as e:
-        print(f"  Gurobi initialization failed: {e}")
-
-    try:
-        torch_solver = TorchLPSolver()
-        print(f"  TorchLP solver available (device: {torch_solver._device})")
-    except Exception as e:
-        print(f"  TorchLP initialization failed: {e}")
-    
-    solvers_to_test = []
-    if gurobi_solver:
-        solvers_to_test.append(("Gurobi", gurobi_solver))
-    if torch_solver:
-        solvers_to_test.append(("TorchLP", torch_solver))
-    
-    if not solvers_to_test:
-        print("  No solvers available!")
-        print("  Will only test conversions without verification")
-    
-    print(f"\n Step 5: Processing all models...")
+    failed_conversions = {}
     
     for idx, (model_id, wrapped_model) in enumerate(successful_models.items(), 1):
         print(f"\n  [{idx}/{len(successful_models)}] Processing '{model_id}'...")
         
-        # === CONVERSION ===
         try:
             net = TorchToACT(wrapped_model).run()
             
-            # Verify the conversion produced a valid net
             if not net.layers:
                 raise ValueError("Net should have layers")
             if net.layers[0].kind != LayerKind.INPUT.value:
@@ -2309,74 +2313,30 @@ def main():
             
             layer_types = " -> ".join([layer.kind for layer in net.layers])
             print(f"    Conversion: {len(net.layers)} layers ({layer_types})")
-            
-            conversion_results[model_id] = "SUCCESS"
-            conversion_success_count += 1
-            
-        except Exception as e:
-            conversion_results[model_id] = f"FAILED: {str(e)[:100]}..."
+            del net
+        except Exception as e:  # noqa: BLE001 — collect every failure, raise below
+            failed_conversions[model_id] = e
             print(f"    Conversion FAILED: {e}")
-            continue  # Skip verification if conversion failed
-        
-        # === VERIFICATION (only if solvers available) ===
-        if solvers_to_test:
-            model_verification = {}
-            
-            for solver_name, solver in solvers_to_test:
-                try:
-                    # TEMPORARILY COMMENTED OUT: Testing if verify_once causes memory issue
-                    # res = verify_once(net, solver=solver, timelimit=30.0)
-                    # status = res.status
-                    status = "SKIPPED"  # Placeholder to test memory usage
-                    model_verification[solver_name] = status
-                    print(f"    Verification ({solver_name}): {status} (verify_once commented out)")
-                    
-                    if status == "UNSAT" or status == "SAT":
-                        verification_success_count += 1
-                        
-                except Exception as e:
-                    model_verification[solver_name] = f"ERROR: {str(e)[:50]}"
-                    print(f"    Verification ({solver_name}): ERROR - {str(e)[:50]}")
-            
-            verification_results[model_id] = model_verification
-        
-        # === MEMORY CLEANUP ===
-        # Free memory from this net immediately (no need to store)
-        del net
         
-        # Clean up memory periodically
         if idx % 10 == 0:
             gc.collect()
             if torch_module.cuda.is_available():
                 torch_module.cuda.empty_cache()
     
-    # === FINAL SUMMARY ===
     total_count = len(successful_models)
     print(f"\nFinal Results:")
-    print(f"  Conversions: {conversion_success_count}/{total_count} ({conversion_success_count/total_count*100:.1f}%)")
+    print(f"  Conversions: {total_count - len(failed_conversions)}/{total_count}")
     
-    if solvers_to_test and verification_results:
-        # Count successful verifications (UNSAT or SAT results)
-        total_verifications = sum(len(v) for v in verification_results.values())
-        successful_verifications = sum(
-            1 for results in verification_results.values() 
-            for status in results.values() 
-            if isinstance(status, str) and status in ["UNSAT", "SAT"]
-        )
-        print(f"  Verifications: {successful_verifications}/{total_verifications} successful")
-    
-    # Print failed conversions if any
-    failed_conversions = {k: v for k, v in conversion_results.items() if v != "SUCCESS"}
-    if failed_conversions:
-        print(f"\n  Failed conversions: {len(failed_conversions)}")
-        for model_id, error in list(failed_conversions.items())[:5]:  # Show first 5
-            print(f"    - {model_id}: {error}")
-    
-    # Print debug file location (GUARDED)
     if PerformanceOptions.debug_tf:
         print(f"\nDebug log written to: {PerformanceOptions.debug_output_file}")
     
-    print("\nTorch->ACT conversion and verification completed!")
+    if failed_conversions:
+        details = "\n  ".join(f"{model_id}: {err}" for model_id, err in failed_conversions.items())
+        raise RuntimeError(
+            f"{len(failed_conversions)}/{total_count} Torch→ACT conversion(s) failed:\n  {details}"
+        )
+    
+    print("\nTorch->ACT conversion completed!")
 
 
 if __name__ == "__main__":
diff --git a/act/pipeline/verification/utils.py b/act/pipeline/verification/utils.py
index 2c6deed78..1053fa735 100644
--- a/act/pipeline/verification/utils.py
+++ b/act/pipeline/verification/utils.py
@@ -14,14 +14,8 @@
 #===---------------------------------------------------------------------===#
 
 import time
-import psutil
 import logging
-import functools
-import threading
-from concurrent.futures import ThreadPoolExecutor, as_completed
-from typing import List, Callable, Any, Dict, Optional, Tuple
-from dataclasses import dataclass
-from contextlib import contextmanager
+from typing import List, Any, Dict, Optional, Tuple
 import torch
 
 logger = logging.getLogger(__name__)
@@ -70,6 +64,26 @@ def _assert_dag(preds: Dict[int, List[int]], succs: Dict[int, List[int]], n_laye
         raise ValueError(f"Layer graph contains a cycle! Nodes: {cycle_nodes}")
 
 
+def _assert_dataflow(layers: List[Any], preds: Dict[int, List[int]]) -> None:
+    """Assert every layer reads its in_vars from its predecessors' out_vars.
+
+    A violation means an edge bypasses a layer (e.g. BatchNorm's SCALE), so
+    abstract interpretation would propagate the bounds of the wrong tensor.
+    """
+    by_id = {layer.id: layer for layer in layers}
+    for layer in layers:
+        layer_preds = preds.get(layer.id, [])
+        if not layer.in_vars or not layer_preds:
+            continue
+        produced = set().union(*(by_id[p].out_vars for p in layer_preds))
+        missing = set(layer.in_vars) - produced
+        assert not missing, (
+            f"Layer {layer.id} ({layer.kind}) reads {len(missing)}/{len(layer.in_vars)} "
+            f"input vars not produced by its predecessors "
+            f"{[(p, by_id[p].kind) for p in layer_preds]}"
+        )
+
+
 def _normalize_axes(axes: Any, rank: int) -> List[int]:
     """Sort + dedupe + normalise possibly-negative axes against ``rank``."""
     return sorted({(a + rank) if a < 0 else a for a in (int(x) for x in axes)})
@@ -138,363 +152,6 @@ def _broadcast_const_to_size(const: torch.Tensor, size: int, dtype: torch.dtype)
     )
 
 
-@dataclass
-class PerformanceMetrics:  # pragma: no cover
-    """Performance metrics for validation operations."""
-    execution_time: float
-    peak_memory_mb: float
-    cpu_usage_percent: float
-    gpu_memory_mb: Optional[float] = None
-
-
-@dataclass
-class ParallelResult:  # pragma: no cover
-    """Result from parallel execution."""
-    results: List[Any]
-    failed_tasks: List[Tuple[int, Exception]]
-    total_time: float
-    metrics: PerformanceMetrics
-
-
-class PerformanceProfiler:  # pragma: no cover
-    """Performance profiling utilities for validation operations."""
-    
-    def __init__(self):
-        self.start_time: Optional[float] = None
-        self.start_memory: Optional[float] = None
-        self.peak_memory: float = 0
-        self.cpu_usage_samples: List[float] = []
-        self._monitoring_thread: Optional[threading.Thread] = None
-        self._stop_monitoring = threading.Event()
-    
-    def start(self) -> None:
-        """Start performance monitoring."""
-        self.start_time = time.time()
-        self.start_memory = self._get_memory_usage()
-        self.peak_memory = self.start_memory
-        self.cpu_usage_samples = []
-        self._stop_monitoring.clear()
-        
-        # Start monitoring thread
-        self._monitoring_thread = threading.Thread(target=self._monitor_resources)
-        self._monitoring_thread.daemon = True
-        self._monitoring_thread.start()
-        
-        logger.debug("Performance profiling started")
-    
-    def stop(self) -> PerformanceMetrics:
-        """Stop monitoring and return performance metrics."""
-        if self.start_time is None:
-            raise RuntimeError("Profiler not started")
-        
-        # Stop monitoring thread
-        self._stop_monitoring.set()
-        if self._monitoring_thread:
-            self._monitoring_thread.join(timeout=1.0)
-        
-        execution_time = time.time() - self.start_time
-        avg_cpu_usage = sum(self.cpu_usage_samples) / len(self.cpu_usage_samples) if self.cpu_usage_samples else 0
-        
-        metrics = PerformanceMetrics(
-            execution_time=execution_time,
-            peak_memory_mb=self.peak_memory,
-            cpu_usage_percent=avg_cpu_usage,
-            gpu_memory_mb=self._get_gpu_memory() if torch.cuda.is_available() else None
-        )
-        
-        logger.debug(f"Performance metrics: {metrics}")
-        return metrics
-    
-    def _monitor_resources(self) -> None:
-        """Monitor resource usage in background thread."""
-        while not self._stop_monitoring.wait(0.1):  # Sample every 100ms
-            try:
-                # Monitor memory
-                current_memory = self._get_memory_usage()
-                self.peak_memory = max(self.peak_memory, current_memory)
-                
-                # Monitor CPU
-                cpu_usage = psutil.cpu_percent(interval=None)
-                self.cpu_usage_samples.append(cpu_usage)
-                
-            except Exception as e:
-                logger.warning(f"Resource monitoring error: {e}")
-    
-    def _get_memory_usage(self) -> float:
-        """Get current memory usage in MB."""
-        process = psutil.Process()
-        return process.memory_info().rss / 1024 / 1024
-    
-    def _get_gpu_memory(self) -> Optional[float]:
-        """Get GPU memory usage in MB."""
-        if not torch.cuda.is_available():
-            return None
-        try:
-            return torch.cuda.memory_allocated() / 1024 / 1024
-        except Exception:
-            return None
-
-
-@contextmanager
-def profile_performance():  # pragma: no cover
-    """Context manager for performance profiling."""
-    profiler = PerformanceProfiler()
-    profiler.start()
-    try:
-        yield profiler
-    finally:
-        metrics = profiler.stop()
-        yield metrics
-
-
-class ParallelExecutor:  # pragma: no cover
-    """Utilities for parallel execution of validation tasks."""
-    
-    def __init__(self, max_workers: Optional[int] = None, timeout: Optional[float] = None):
-        """
-        Initialize parallel executor.
-        
-        Args:
-            max_workers: Maximum number of worker threads
-            timeout: Timeout for individual tasks in seconds
-        """
-        self.max_workers = max_workers or min(32, (psutil.cpu_count() or 1) + 4)
-        self.timeout = timeout
-    
-    def execute_parallel(self, 
-                        tasks: List[Callable],
-                        task_args: Optional[List[Tuple]] = None,
-                        task_kwargs: Optional[List[Dict]] = None) -> ParallelResult:
-        """
-        Execute tasks in parallel.
-        
-        Args:
-            tasks: List of callable tasks to execute
-            task_args: List of argument tuples for each task
-            task_kwargs: List of keyword argument dicts for each task
-            
-        Returns:
-            ParallelResult with results and performance metrics
-        """
-        if task_args is None:
-            task_args = [() for _ in tasks]
-        if task_kwargs is None:
-            task_kwargs = [{} for _ in tasks]
-        
-        if len(tasks) != len(task_args) or len(tasks) != len(task_kwargs):
-            raise ValueError("tasks, task_args, and task_kwargs must have same length")
-        
-        results = []
-        failed_tasks = []
-        
-        with profile_performance() as profiler:
-            with ThreadPoolExecutor(max_workers=self.max_workers) as executor:
-                # Submit all tasks
-                future_to_index = {
-                    executor.submit(task, *args, **kwargs): i
-                    for i, (task, args, kwargs) in enumerate(zip(tasks, task_args, task_kwargs))
-                }
-                
-                # Collect results
-                for future in as_completed(future_to_index, timeout=self.timeout):
-                    task_index = future_to_index[future]
-                    try:
-                        result = future.result()
-                        results.append((task_index, result))
-                    except Exception as e:
-                        failed_tasks.append((task_index, e))
-                        logger.error(f"Task {task_index} failed: {e}")
-        
-        # Sort results by original task index
-        results.sort(key=lambda x: x[0])
-        sorted_results = [result for _, result in results]
-        
-        metrics = profiler.stop()
-        
-        return ParallelResult(
-            results=sorted_results,
-            failed_tasks=failed_tasks,
-            total_time=metrics.execution_time,
-            metrics=metrics
-        )
-    
-    def map_parallel(self, func: Callable, items: List[Any]) -> ParallelResult:
-        """
-        Apply function to list of items in parallel.
-        
-        Args:
-            func: Function to apply to each item
-            items: List of items to process
-            
-        Returns:
-            ParallelResult with mapped results
-        """
-        tasks = [func for _ in items]
-        task_args = [(item,) for item in items]
-        
-        return self.execute_parallel(tasks, task_args)
-
-
-def print_memory_usage(prefix: str = "") -> None:  # pragma: no cover
-    """Print current memory usage information."""
-    process = psutil.Process()
-    memory_info = process.memory_info()
-    
-    memory_mb = memory_info.rss / 1024 / 1024
-    cpu_percent = process.cpu_percent()
-    
-    gpu_info = ""
-    if torch.cuda.is_available():
-        gpu_memory_mb = torch.cuda.memory_allocated() / 1024 / 1024
-        gpu_max_mb = torch.cuda.max_memory_allocated() / 1024 / 1024
-        gpu_info = f", GPU: {gpu_memory_mb:.1f}MB (max: {gpu_max_mb:.1f}MB)"
-    
-    logger.info(f"{prefix}Memory: {memory_mb:.1f}MB, CPU: {cpu_percent:.1f}%{gpu_info}")
-
-
-def clear_torch_cache() -> None:  # pragma: no cover
-    """Clear PyTorch GPU cache if available."""
-    if torch.cuda.is_available():
-        torch.cuda.empty_cache()
-        logger.debug("Cleared PyTorch GPU cache")
-
-
-def setup_logging(level: str = "INFO", format_str: Optional[str] = None) -> None:  # pragma: no cover
-    """
-    Setup logging configuration for the pipeline.
-    
-    Args:
-        level: Logging level (DEBUG, INFO, WARNING, ERROR)
-        format_str: Custom format string for log messages
-    """
-    if format_str is None:
-        format_str = "%(asctime)s - %(name)s - %(levelname)s - %(message)s"
-    
-    # Ensure log file goes to pipeline/log directory
-    import os
-    from pathlib import Path
-    pipeline_dir = Path(__file__).parent
-    log_dir = pipeline_dir / "log"
-    log_dir.mkdir(exist_ok=True)
-    log_file_path = log_dir / "pipeline_tests.log"
-    
-    logging.basicConfig(
-        level=getattr(logging, level.upper()),
-        format=format_str,
-        handlers=[
-            logging.StreamHandler(),
-            logging.FileHandler(log_file_path)
-        ]
-    )
-    
-    # Reduce noise from some libraries
-    logging.getLogger("matplotlib").setLevel(logging.WARNING)
-    logging.getLogger("PIL").setLevel(logging.WARNING)
-
-
-def retry_on_failure(max_retries: int = 3, delay: float = 1.0, backoff: float = 2.0):  # pragma: no cover
-    """
-    Decorator to retry function on failure.
-    
-    Args:
-        max_retries: Maximum number of retry attempts
-        delay: Initial delay between retries in seconds
-        backoff: Backoff multiplier for delay
-    """
-    def decorator(func):
-        @functools.wraps(func)
-        def wrapper(*args, **kwargs):
-            current_delay = delay
-            last_exception = None
-            
-            for attempt in range(max_retries + 1):
-                try:
-                    return func(*args, **kwargs)
-                except Exception as e:
-                    last_exception = e
-                    if attempt < max_retries:
-                        logger.warning(f"Attempt {attempt + 1} failed for {func.__name__}: {e}")
-                        time.sleep(current_delay)
-                        current_delay *= backoff
-                    else:
-                        logger.error(f"All {max_retries + 1} attempts failed for {func.__name__}")
-            
-            raise last_exception
-        
-        return wrapper
-    return decorator
-
-
-def timeout_handler(timeout_seconds: float):  # pragma: no cover
-    """
-    Decorator to add timeout to function execution.
-    
-    Args:
-        timeout_seconds: Timeout in seconds
-    """
-    def decorator(func):
-        @functools.wraps(func)
-        def wrapper(*args, **kwargs):
-            import signal
-            
-            def timeout_signal_handler(signum, frame):
-                raise TimeoutError(f"Function {func.__name__} timed out after {timeout_seconds} seconds")
-            
-            # Set up signal handler
-            old_handler = signal.signal(signal.SIGALRM, timeout_signal_handler)
-            signal.alarm(int(timeout_seconds))
-            
-            try:
-                result = func(*args, **kwargs)
-            finally:
-                # Restore old signal handler
-                signal.alarm(0)
-                signal.signal(signal.SIGALRM, old_handler)
-            
-            return result
-        
-        return wrapper
-    return decorator
-
-
-class ProgressTracker:  # pragma: no cover
-    """Track progress of long-running operations."""
-    
-    def __init__(self, total_items: int, description: str = "Processing"):
-        self.total_items = total_items
-        self.description = description
-        self.completed_items = 0
-        self.start_time = time.time()
-    
-    def update(self, completed: int = 1) -> None:
-        """Update progress by specified number of completed items."""
-        self.completed_items += completed
-        self._print_progress()
-    
-    def _print_progress(self) -> None:
-        """Print current progress."""
-        if self.total_items == 0:
-            return
-        
-        percentage = (self.completed_items / self.total_items) * 100
-        elapsed_time = time.time() - self.start_time
-        
-        if self.completed_items > 0:
-            eta = (elapsed_time / self.completed_items) * (self.total_items - self.completed_items)
-            eta_str = f", ETA: {eta:.1f}s"
-        else:
-            eta_str = ""
-        
-        logger.info(f"{self.description}: {self.completed_items}/{self.total_items} "
-                   f"({percentage:.1f}%) - {elapsed_time:.1f}s elapsed{eta_str}")
-    
-    def finish(self) -> None:
-        """Mark progress as complete."""
-        self.completed_items = self.total_items
-        elapsed_time = time.time() - self.start_time
-        logger.info(f"{self.description} completed in {elapsed_time:.1f}s")
-
-
 # -----------------------------------------------------------------------------
 # ONNX -> ACT layer handlers (bound onto _LayerGraphBuilder via setattr in
 # torch2act.py). Kept here only to keep that file manageable; ``self`` is always
@@ -1257,10 +914,7 @@ def _convert_OnnxMinMax(self, mod: nn.Module, node: fx.Node) -> None:
             raise ValueError(f"OnnxMinMax at {node.name}: '{n.name}' not registered")
     xv, yv = self.node_outputs[args[0].name], self.node_outputs[args[1].name]
     xs, ys = self.node_shapes[args[0].name], self.node_shapes[args[1].name]
-    try:
-        output_shape = tuple(int(d) for d in torch.broadcast_shapes(xs, ys))
-    except RuntimeError:
-        output_shape = xs if _prod(xs) >= _prod(ys) else ys
+    output_shape = tuple(int(d) for d in torch.broadcast_shapes(xs, ys))
     out_vars = self._alloc_ids(_prod(output_shape) or 1)
     layer_id = self._add_layer(
         kind.value,
@@ -1335,14 +989,11 @@ def _convert_OnnxWhere(self, mod: nn.Module, node: fx.Node) -> None:
     cv = self.node_outputs[args[0].name]
     xv = self.node_outputs[args[1].name]
     yv = self.node_outputs[args[2].name]
-    try:
-        output_shape = tuple(int(d) for d in torch.broadcast_shapes(
-            self.node_shapes[args[0].name],
-            self.node_shapes[args[1].name],
-            self.node_shapes[args[2].name],
-        ))
-    except RuntimeError:
-        output_shape = self.node_shapes[args[1].name]
+    output_shape = tuple(int(d) for d in torch.broadcast_shapes(
+        self.node_shapes[args[0].name],
+        self.node_shapes[args[1].name],
+        self.node_shapes[args[2].name],
+    ))
     out_vars = self._alloc_ids(_prod(output_shape) or 1)
     layer_id = self._add_layer(
         LayerKind.WHERE.value,
@@ -1539,10 +1190,7 @@ def _convert_OnnxCompare(self, mod: nn.Module, node: fx.Node) -> None:
             raise ValueError(f"OnnxCompare at {node.name}: '{n.name}' not registered")
     xv, yv = self.node_outputs[x_node.name], self.node_outputs[y_node.name]
     xs, ys = self.node_shapes[x_node.name], self.node_shapes[y_node.name]
-    try:
-        output_shape = tuple(int(d) for d in torch.broadcast_shapes(xs, ys))
-    except RuntimeError:
-        output_shape = xs if _prod(xs) >= _prod(ys) else ys
+    output_shape = tuple(int(d) for d in torch.broadcast_shapes(xs, ys))
     out_vars = self._alloc_ids(_prod(output_shape) or 1)
     layer_id = self._add_layer(
         LayerKind.COMPARE.value,
diff --git a/act/pipeline/verification/validate_verifier.py b/act/pipeline/verification/validate_verifier.py
index d1eea42c8..b280ad178 100644
--- a/act/pipeline/verification/validate_verifier.py
+++ b/act/pipeline/verification/validate_verifier.py
@@ -319,24 +319,17 @@ def _batchify_assert_layer(self, L: Layer, target_B: int) -> None:
                 (v for v in high.values() if torch.is_tensor(v)), None
             )
         )
-        try:
-            spec = OutputSpec(kind=kind, **high)
-            new_params = spec.encode_linear(
-                B=target_B,
-                n_out=n_out,
-                device=ref.device if ref is not None else torch.device(self.device),
-                dtype=(
-                    ref.dtype
-                    if ref is not None and ref.dtype.is_floating_point
-                    else self.dtype
-                ),
-            )
-        except Exception as e:
-            logger.warning(
-                f"_batchify_assert_layer({kind}) at B={target_B}: "
-                f"re-encode failed: {e}"
-            )
-            return
+        spec = OutputSpec(kind=kind, **high)
+        new_params = spec.encode_linear(
+            B=target_B,
+            n_out=n_out,
+            device=ref.device if ref is not None else torch.device(self.device),
+            dtype=(
+                ref.dtype
+                if ref is not None and ref.dtype.is_floating_point
+                else self.dtype
+            ),
+        )
 
         L.params.clear()
         L.params.update(new_params)
diff --git a/act/util/device_manager.py b/act/util/device_manager.py
index 3b99ea431..e92f52b48 100644
--- a/act/util/device_manager.py
+++ b/act/util/device_manager.py
@@ -5,10 +5,8 @@
 import torch
 from typing import Tuple, Optional
 
-try:
+if hasattr(torch.sparse, "check_sparse_tensor_invariants"):
     torch.sparse.check_sparse_tensor_invariants.disable()
-except Exception:
-    pass
 
 # Global initialization state
 _INITIALIZED = False
@@ -66,61 +64,50 @@ def initialize_device(device: str, dtype: str) -> None:
     """
     global _INITIALIZED
     
-    try:
-        # Handle gpu/cuda aliasing
-        if device == 'gpu':
-            device = 'cuda'
-            print(f"🔄 Device alias: 'gpu' → 'cuda'")
+    # Handle gpu/cuda aliasing
+    if device == 'gpu':
+        device = 'cuda'
+        print(f"🔄 Device alias: 'gpu' → 'cuda'")
         
-        # Determine target device
-        if device == 'cpu':
-            target_device = torch.device("cpu")
-        elif device == 'cuda':
-            if torch.cuda.is_available():
-                target_device = torch.device("cuda:0")
-            else:
-                target_device = torch.device("cpu")
-                print(f"⚠️ CUDA not available, falling back to CPU")
-        elif device == 'mps':
-            if hasattr(torch.backends, 'mps') and torch.backends.mps.is_available():
-                target_device = torch.device("mps")
-            else:
-                target_device = torch.device("cpu")
-                print(f"⚠️ MPS not available, falling back to CPU")
-        else:
-            # Unknown device, default to CPU
-            target_device = torch.device("cpu")
-            print(f"⚠️ Unknown device '{device}', using CPU")
+    # Determine target device. CLI defaults already select an available device,
+    # so an unavailable explicit request is a configuration error.
+    if device == 'cpu':
+        target_device = torch.device("cpu")
+    elif device == 'cuda':
+        if not torch.cuda.is_available():
+            raise RuntimeError("CUDA device requested but CUDA is not available")
+        target_device = torch.device("cuda:0")
+    elif device == 'mps':
+        if not hasattr(torch.backends, 'mps') or not torch.backends.mps.is_available():
+            raise RuntimeError("MPS device requested but MPS is not available")
+        target_device = torch.device("mps")
+    else:
+        raise ValueError(
+            f"Unknown device {device!r}; expected one of 'cpu', 'cuda', 'gpu', or 'mps'"
+        )
         
-        # Determine target dtype
-        if dtype == 'float32':
-            target_dtype = torch.float32
-        elif dtype == 'float64':
-            target_dtype = torch.float64
-        else:
-            # Unknown dtype, default to float64
-            target_dtype = torch.float64
-            print(f"⚠️ Unknown dtype '{dtype}', using float64")
+    # Determine target dtype.
+    if dtype == 'float32':
+        target_dtype = torch.float32
+    elif dtype == 'float64':
+        target_dtype = torch.float64
+    else:
+        raise ValueError(
+            f"Unknown dtype {dtype!r}; expected 'float32' or 'float64'"
+        )
         
-        # Set PyTorch global defaults
-        torch.set_default_dtype(target_dtype)
-        if hasattr(torch, 'set_default_device'):
-            torch.set_default_device(target_device)
+    # Set PyTorch global defaults
+    torch.set_default_dtype(target_dtype)
+    if hasattr(torch, 'set_default_device'):
+        torch.set_default_device(target_device)
 
-        precision = _apply_precision_policy()
+    precision = _apply_precision_policy()
 
-        print(
-            f"✅ Device Manager Initialized: device={target_device}, "
-            f"dtype={target_dtype}, {precision}"
-        )
-        _INITIALIZED = True
-        
-    except Exception as e:
-        print(f"❌ Device initialization failed: {e}")
-        print(f"   Falling back to CPU + float64")
-        torch.set_default_dtype(torch.float64)
-        _apply_precision_policy()
-        _INITIALIZED = True
+    print(
+        f"✅ Device Manager Initialized: device={target_device}, "
+        f"dtype={target_dtype}, {precision}"
+    )
+    _INITIALIZED = True
 
 
 def get_default_device() -> torch.device:
@@ -133,10 +120,7 @@ def get_default_device() -> torch.device:
     _ensure_initialized()
     
     if hasattr(torch, 'get_default_device'):
-        try:
-            return torch.get_default_device()
-        except:
-            return torch.device("cpu")
+        return torch.get_default_device()
     else:
         # For older PyTorch versions, check where a test tensor is created
         test_tensor = torch.zeros(1)
@@ -186,19 +170,13 @@ def _ensure_initialized():
         device = 'cuda' if torch.cuda.is_available() else 'cpu'
         dtype = 'float64'
         
-        # Initialize with defaults (no print statements for lazy init)
-        try:
-            target_device = torch.device("cuda:0") if device == 'cuda' else torch.device("cpu")
-            target_dtype = torch.float64
-            
-            torch.set_default_dtype(target_dtype)
-            if hasattr(torch, 'set_default_device'):
-                torch.set_default_device(target_device)
-            
-            _apply_precision_policy()
-            _INITIALIZED = True
-        except Exception:
-            # Silent fallback to CPU + float64
-            torch.set_default_dtype(torch.float64)
-            _apply_precision_policy()
-            _INITIALIZED = True
+        # Initialize with defaults (no print statements for lazy init).
+        target_device = torch.device("cuda:0") if device == 'cuda' else torch.device("cpu")
+        target_dtype = torch.float64
+
+        torch.set_default_dtype(target_dtype)
+        if hasattr(torch, 'set_default_device'):
+            torch.set_default_device(target_device)
+
+        _apply_precision_policy()
+        _INITIALIZED = True
diff --git a/act/util/format_utils.py b/act/util/format_utils.py
index 31bd82e77..3042bb764 100644
--- a/act/util/format_utils.py
+++ b/act/util/format_utils.py
@@ -33,14 +33,16 @@ def format_bytes(size_bytes: Union[int, float], precision: int = 1) -> str:
 
 
 def dir_size(path: Union[str, Path]) -> int:
-    """Return total size in bytes of all files under ``path`` (0 on error)."""
+    """Return total size in bytes of all files under ``path``."""
+    root = Path(path)
+    if not root.exists():
+        raise FileNotFoundError(f"Directory does not exist: {root}")
+    if not root.is_dir():
+        raise NotADirectoryError(f"Expected a directory, got: {root}")
     total = 0
-    try:
-        for item in Path(path).rglob("*"):
-            if item.is_file():
-                total += item.stat().st_size
-    except Exception:
-        pass
+    for item in root.rglob("*"):
+        if item.is_file():
+            total += item.stat().st_size
     return total
 
 
diff --git a/act/util/model_inference.py b/act/util/model_inference.py
index 4753ba6b7..07c8b8bc7 100644
--- a/act/util/model_inference.py
+++ b/act/util/model_inference.py
@@ -42,10 +42,14 @@ def infer_single_model(combo_id: Union[str, Tuple], model: nn.Module, input_tens
             output = model(input_tensor)
             # Extract tensor if model returns dict (VerifiableModel)
             if isinstance(output, dict):
+                if 'output' not in output:
+                    raise KeyError(
+                        f"Model {combo_id!r} returned a dictionary without an 'output' entry"
+                    )
                 output = output['output']
             return True, output, None
-    except Exception as e:
-        return False, None, str(e)[:100]
+    except Exception as exc:
+        raise RuntimeError(f"Model inference failed for {combo_id!r}: {exc}") from exc
 
 
 # Main model inference function
@@ -65,8 +69,9 @@ def model_inference(models: Dict[Union[str, Tuple], nn.Module]) -> Dict[Union[st
     
     # Handle case where no models were generated
     if not models:
-        print("⚠️  No models to test - check spec generation and synthesis configuration")
-        return {}
+        raise ValueError(
+            "No models to test; check spec generation and synthesis configuration"
+        )
     
     success_count = 0
     failure_count = 0
@@ -78,15 +83,17 @@ def model_inference(models: Dict[Union[str, Tuple], nn.Module]) -> Dict[Union[st
         # Extract input and label from InputLayer (named child on VerifiableModel)
         input_layer = model.input_layer
         if not hasattr(input_layer, 'input_tensor'):
-            print(f"⚠️  Model {combo_id} missing input_tensor in InputLayer")
-            failure_count += 1
-            continue
+            raise AttributeError(
+                f"Model {combo_id!r} InputLayer is missing input_tensor"
+            )
         
         test_input = input_layer.input_tensor
         test_label = input_layer.label
         
         # Move input to same device as model
-        model_device = next(model.parameters()).device
+        # Parameter-free models (e.g. pure-constant ONNX nets) keep the input's device.
+        first_param = next(model.parameters(), None)
+        model_device = first_param.device if first_param is not None else test_input.device
         test_input = test_input.to(model_device)
         
         # Parse combo_id: handle tuple keys (dataset, model, in_kind, out_kind)
@@ -107,9 +114,12 @@ def model_inference(models: Dict[Union[str, Tuple], nn.Module]) -> Dict[Union[st
         success, output, error_msg = infer_single_model(combo_id, model, test_input)
         
         if success:
-            # Validate prediction against ground truth label tensor (N,), output is (N, num_classes)
-            pred_classes = output.argmax(dim=1)  # (N,)
-            is_correct = (pred_classes == test_label).all().item()
+            # Validate prediction against ground truth label tensor (N,), output is (N, num_classes).
+            # Unlabelled or non-classification outputs (e.g. VNNLIB safety nets) have no accuracy.
+            is_correct = False
+            if test_label is not None and test_label.numel() > 0 and output.dim() >= 2:
+                pred_classes = output.argmax(dim=1)  # (N,)
+                is_correct = (pred_classes == test_label).all().item()
             
             success_count += 1
             if is_correct:
@@ -137,4 +147,3 @@ def model_inference(models: Dict[Union[str, Tuple], nn.Module]) -> Dict[Union[st
         print(f"   💡 Tip: Use domain-matched combinations (mnist+mnist, cifar+cifar) for 100% success")
     
     return successful_models
-
diff --git a/act/util/stats.py b/act/util/stats.py
index 42ffd454e..af59c7bec 100644
--- a/act/util/stats.py
+++ b/act/util/stats.py
@@ -23,13 +23,11 @@
 #
 #===----------------------------------------------------------------------===#
 
-import os
 import torch
 from enum import Enum
 from dataclasses import dataclass, field
-from typing import Dict, Any, List, Tuple, Optional
+from typing import Dict, Any, List, Optional
 
-from act.util.format_utils import rule
 
 
 # =============================================================================
@@ -153,382 +151,3 @@ def to_verify_results(self, *, source: str = "dual_bound") -> List["VerifyResult
                 },
             ))
         return results
-
-
-# =============================================================================
-# Statistics and Logging Utilities
-# =============================================================================
-
-class ACTStats:
-    """
-    Utility class for monitoring and reporting memory usage during verification.
-    
-    Provides comprehensive memory monitoring including system memory, process memory,
-    and GPU memory statistics. Gracefully handles missing dependencies.
-    """
-    
-    @staticmethod
-    def print_memory_usage(stage_name: str = "") -> float:
-        """
-        Print comprehensive memory usage statistics for the current process and system.
-        
-        Reports process memory usage, system memory statistics, and GPU memory
-        information when available. Handles missing psutil dependency gracefully.
-        
-        Args:
-            stage_name: Optional label for the memory report stage
-            
-        Returns:
-            float: Process memory usage in MB, or 0 if psutil is unavailable
-        """
-        try:
-            import psutil
-            process = psutil.Process(os.getpid())
-            memory_info = process.memory_info()
-            memory_mb = memory_info.rss / 1024 / 1024
-
-            system_memory = psutil.virtual_memory()
-            total_mb = system_memory.total / 1024 / 1024
-            available_mb = system_memory.available / 1024 / 1024
-            used_percent = (memory_mb / total_mb) * 100
-
-            print(f"[{stage_name}] Memory Usage:")
-            print(f"Process: {memory_mb:.1f} MB ({used_percent:.1f}% of total)")
-            print(f"System: {total_mb:.1f} MB total, {available_mb:.1f} MB available")
-
-            if torch.cuda.is_available():
-                gpu_memory_mb = torch.cuda.memory_allocated() / 1024 / 1024
-                gpu_cached_mb = torch.cuda.memory_reserved() / 1024 / 1024
-                print(f"GPU: {gpu_memory_mb:.1f} MB allocated, {gpu_cached_mb:.1f} MB cached")
-
-            return memory_mb
-            
-        except ImportError:
-            print(f"⚠️ [{stage_name}] psutil not available, cannot monitor memory")
-            return 0.0
-        except Exception as e:
-            print(f"⚠️ [{stage_name}] Error monitoring memory: {e}")
-            return 0.0
-    
-    @classmethod
-    def get_memory_usage_mb(cls) -> float:
-        """
-        Get current process memory usage in MB without printing.
-        
-        Returns:
-            float: Process memory usage in MB, or 0 if psutil is unavailable
-        """
-        try:
-            import psutil
-            process = psutil.Process(os.getpid())
-            memory_info = process.memory_info()
-            return memory_info.rss / 1024 / 1024
-        except (ImportError, Exception):
-            return 0.0
-    
-    @classmethod
-    def get_current_memory_usage(cls) -> float:
-        """
-        Get current memory usage in MB (GPU if available, otherwise CPU).
-        
-        This is an enhanced version that automatically detects the best memory
-        source (GPU vs CPU) for tracking during bounds propagation.
-        
-        Returns:
-            float: Current memory usage in MB
-        """
-        try:
-            if torch.cuda.is_available() and torch.cuda.device_count() > 0:
-                # Get GPU memory usage
-                gpu_memory_bytes = torch.cuda.memory_allocated()
-                return gpu_memory_bytes / (1024 * 1024)  # Convert to MB
-            else:
-                # Get CPU memory usage for current process
-                import psutil
-                process = psutil.Process(os.getpid())
-                cpu_memory_bytes = process.memory_info().rss
-                return cpu_memory_bytes / (1024 * 1024)  # Convert to MB
-        except (ImportError, Exception):
-            # Fallback if psutil unavailable or memory monitoring fails
-            return 0.0
-    
-    @classmethod
-    def get_gpu_memory_info(cls) -> Tuple[float, float]:
-        """
-        Get GPU memory info (available, total) in MB.
-        
-        Returns:
-            tuple: (available_memory_mb, total_memory_mb) - (0.0, 0.0) if no GPU
-        """
-        try:
-            if torch.cuda.is_available() and torch.cuda.device_count() > 0:
-                total_memory = torch.cuda.get_device_properties(0).total_memory
-                allocated_memory = torch.cuda.memory_allocated()
-                available_memory = total_memory - allocated_memory
-                return available_memory / (1024 * 1024), total_memory / (1024 * 1024)
-            else:
-                return 0.0, 0.0
-        except Exception:
-            return 0.0, 0.0
-    
-    @classmethod
-    def get_cpu_memory_usage(cls) -> float:
-        """
-        Get CPU memory usage for current process in MB.
-        
-        Returns:
-            float: CPU memory usage in MB, or 0.0 if psutil unavailable
-        """
-        try:
-            import psutil
-            process = psutil.Process(os.getpid())
-            return process.memory_info().rss / (1024 * 1024)
-        except (ImportError, Exception):
-            return 0.0
-    
-    @staticmethod
-    def print_verification_stats(prediction_stats: Dict[str, Any]) -> None:
-        """
-        Print verification statistics from the prediction stats.
-        
-        Args:
-            prediction_stats: Dictionary containing various verification statistics
-        """
-        # Hardcode verification_result_stat_dict as empty for now
-        verification_result_stat_dict = {}  
-        
-        print("\n📊 Verification Results Summary:")
-        
-        # Display known statistics
-        known_keys = ['total', 'safe', 'unsafe', 'timeout', 'model_infer_failure']
-        for key in known_keys:
-            if key in prediction_stats:
-                print(f"  {key}: {prediction_stats[key]}")
-        
-        # Display any additional statistics
-        additional_stats = {k: v for k, v in prediction_stats.items() if k not in known_keys}
-        if additional_stats:
-            print("  Additional stats:")
-            for key, value in additional_stats.items():
-                print(f"    {key}: {value}")
-        
-        # Display verification result statistics if available
-        if verification_result_stat_dict:
-            print("\n🔍 Verification VerifyStatus Distribution:")
-            for status, count in verification_result_stat_dict.items():
-                print(f"  {status}: {count}")
-        
-        print(rule(50, "-"))
-
-    @staticmethod
-    def print_final_verification_summary(results: List) -> Any:
-        """
-        Print final verification results summary and return the overall verdict.
-        
-        Args:
-            results: List of VerifyStatus for all verified samples
-            
-        Returns:
-            Overall VerifyStatus (CERTIFIED if all safe, FALSIFIED if any unsafe, UNKNOWN otherwise)
-        """
-        # VerifyStatus is now defined at module level in this file
-        
-        print("\n" + "🏆" + rule(70) + "🏆")
-        print("📊 Final verification results summary")
-        print("🏆" + rule(70) + "🏆")
-
-        for idx, result in enumerate(results):
-            print(f"Sample {idx+1}: {result.name}")
-
-        print(rule(60, "-"))
-
-        certified_count = sum(1 for r in results if r == VerifyStatus.CERTIFIED)
-        falsified_count = sum(1 for r in results if r == VerifyStatus.FALSIFIED)
-        model_infer_failure_count = sum(1 for r in results if r == VerifyStatus.MODEL_INFER_FAILURE)
-        unknown_count = sum(1 for r in results if r == VerifyStatus.UNKNOWN)
-        total_count = len(results)
-
-        valid_count = total_count - model_infer_failure_count
-
-        print("Verification statistics:")
-        print(f"Total samples: {total_count}")
-        print(f"✅ CERTIFIED (safe): {certified_count} ")
-        print(f"❌ FALSIFIED (unsafe): {falsified_count} ")
-        print(f"⚠️  MODEL_INFER_FAILURE (model inference failed): {model_infer_failure_count} ")
-        print(f"❓ UNKNOWN: {unknown_count} ")
-        print(f"🔍 Valid verification samples: {valid_count} ")
-
-        if valid_count > 0:
-            certified_percentage = (certified_count / valid_count) * 100
-            falsified_percentage = (falsified_count / valid_count) * 100
-            print(f"📊 CERTIFIED over valid samples: {certified_percentage:.2f}% ({certified_count}/{valid_count})")
-            print(f"📊 FALSIFIED over valid samples: {falsified_percentage:.2f}% ({falsified_count}/{valid_count})")
-        else:
-            print("  ⚠️  No valid verification samples")
-
-        if total_count > 0:
-            certified_total_percentage = (certified_count / total_count) * 100
-            falsified_total_percentage = (falsified_count / total_count) * 100
-            model_infer_failure_percentage = (model_infer_failure_count / total_count) * 100
-            print(f"📊 CERTIFIED over total: {certified_total_percentage:.2f}% ({certified_count}/{total_count})")
-            print(f"📊 FALSIFIED over total: {falsified_total_percentage:.2f}% ({falsified_count}/{total_count})")
-            print(f"📊 MODEL_INFER_FAILURE over total: {model_infer_failure_percentage:.2f}% ({model_infer_failure_count}/{total_count})")
-
-        print(rule(60, "-"))
-
-        if all(r == VerifyStatus.CERTIFIED for r in results):
-            final_result = VerifyStatus.CERTIFIED
-            print("✅ Final Result: CERTIFIED - all samples verified safe")
-        elif any(r == VerifyStatus.FALSIFIED for r in results):
-            final_result = VerifyStatus.FALSIFIED
-            print("❌ Final Result: FALSIFIED - at least one sample violates the property")
-        else:
-            final_result = VerifyStatus.UNKNOWN
-            print("❓ Final Result: UNKNOWN - inconclusive")
-
-        print("🏆" + rule(70) + "🏆")
-        return final_result
-
-
-class ACTLog:
-    """
-    Centralized logging utilities for the Abstract Constraints Transformer (ACT).
-    
-    Provides structured logging methods for prediction validation, constraint application,
-    and verification processes with consistent formatting and emoji indicators.
-    """
-    
-    @staticmethod
-    def log_correct_prediction(
-        predicted_label: int, 
-        ground_truth_label: int, 
-        sample_index: int,
-        verbose: bool = True
-    ) -> None:
-        """Log successful prediction with verbose output."""
-        if verbose:
-            print(f"✅ Sample {sample_index + 1} Clean Prediction: Correct "
-                  f"(pred: {predicted_label}, true: {ground_truth_label})")
-    
-    @staticmethod
-    def log_incorrect_prediction(
-        predicted_label: int, 
-        ground_truth_label: int, 
-        sample_index: int,
-        verbose: bool = True
-    ) -> None:
-        """Log failed prediction with verbose output."""
-        if verbose:
-            print(f"❌ Sample {sample_index + 1} Clean Prediction: Incorrect "
-                  f"(pred: {predicted_label}, true: {ground_truth_label})")
-            print("⚠️  Skipping verification - clean prediction already incorrect")
-    
-    @staticmethod
-    def log_prediction_failure(error: Exception) -> None:
-        """Log prediction validation failure."""
-        print(f"❌ Clean prediction validation failed: {error}")
-    
-    @staticmethod
-    def log_constraint_application_start(cache_type_name: str, constraint_count: int, verbose: bool = True) -> None:
-        """Log the start of constraint application process."""
-        if verbose:
-            print(f"[Bounds Fix] Applying {constraint_count} ReLU constraints "
-                  f"to layer bounds cache")
-            print(f"[Bounds Fix] Using {cache_type_name} bounds cache")
-    
-    @staticmethod
-    def log_constraint_processing(
-        layer_name: str, 
-        neuron_index: int, 
-        activation_type: str,
-        verbose: bool = True
-    ) -> None:
-        """Log individual constraint processing."""
-        if verbose:
-            print(f"[Bounds Fix] Processing constraint: "
-                  f"{layer_name}[{neuron_index}] = {activation_type}")
-    
-    @staticmethod
-    def log_constraint_application_complete(verbose: bool = True) -> None:
-        """Log successful completion of constraint application."""
-        if verbose:
-            print("✅ [Bounds Fix] ReLU constraint application done")
-    
-    @staticmethod
-    def log_no_bounds_cache_warning(verbose: bool = True) -> None:
-        """Log warning when no bounds cache is available."""
-        if verbose:
-            print("⚠️  No layer bounds cache found, skipping constraint application")
-    
-    @staticmethod
-    def log_label_warning(sample_index: int) -> None:
-        """Log warning when ground truth label cannot be found."""
-        print(f"⚠️  Could not get true label for sample {sample_index+1}, using default label 0")
-    
-    @staticmethod
-    def log_relu_constraints_set(constraints: List, verbose: bool = True) -> None:
-        """Log ReLU constraint configuration."""
-        if verbose:
-            if constraints:
-                print(f"Set ReLU constraints: {len(constraints)} constraints")
-                for constraint in constraints:
-                    print(f"{constraint['layer']}[{constraint['neuron_idx']}] = {constraint['constraint_type']}")
-            else:
-                print(f"Cleared ReLU constraints")
-    
-    @staticmethod
-    def log_constraint_error(message: str, verbose: bool = True) -> None:
-        """Log constraint processing errors."""
-        if verbose:
-            print(f"⚠️  {message}")
-    
-    @staticmethod
-    def log_constraint_bound_update(
-        constraint_type: str, 
-        neuron_index: int, 
-        original_bound: float, 
-        new_bound: float, 
-        verbose: bool = True
-    ) -> None:
-        """Log individual bound constraint updates."""
-        if verbose:
-            print(f"{constraint_type} constraint: neuron {neuron_index} "
-                  f"{'ub' if constraint_type == 'inactive' else 'lb'}: {original_bound:.6f} → {new_bound:.6f}")
-    
-    @staticmethod
-    def log_verification_info(message: str) -> None:
-        """Log general verification information."""
-        print(f"{message}")
-    
-    @staticmethod
-    def log_verification_warning(message: str) -> None:
-        """Log verification warnings."""
-        print(f"Warning: {message}")
-    
-    @staticmethod
-    def log_bab_start(sample_idx: int) -> None:
-        """Log BaB specification refinement start."""
-        print(f"Starting generic BaB specification refinement verification (sample {sample_idx})")
-        print(f"Framework: theoretically-aligned specification refinement")
-    
-    @staticmethod
-    def log_bab_results(
-        status_name: str, 
-        total_subproblems: int, 
-        spurious_count: int, 
-        has_real_counterexample: bool, 
-        max_depth: int, 
-        total_time: float
-    ) -> None:
-        """Log BaB verification results."""
-        print(f"Specification refinement verification finished: {status_name}")
-        print(f"Total subproblems: {total_subproblems}")
-        print(f"Spurious counterexamples: {spurious_count}")
-        print(f"Real counterexample: {'Yes' if has_real_counterexample else 'No'}")
-        print(f"Max depth: {max_depth}")
-        print(f"Total time: {total_time:.2f}s")
-    
-    @staticmethod
-    def log_bab_error(error: Exception) -> None:
-        """Log BaB verification errors."""
-        print(f"⚠️ Specification refinement verification error: {error}")
\ No newline at end of file