diff options
| -rw-r--r-- | src/checker_set.rs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs index 5410dfe..db47c14 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -307,6 +307,9 @@ impl CheckerState { } }; + // for each arm, recurse with a concrete value (if we have one) + // otherwise fall back to hypothetical elements; in the former + // case record the end result let mut computed_output = None; for arm in arms { let SetField { field_set, .. } = self.lookup_variant_field(&arm.tag)?; @@ -326,6 +329,11 @@ impl CheckerState { { new_context.add_element(binding_name, inner.clone().into(), binding_set)?; let output = new_context.check_element(arm.body.clone().into(), set)?; + if matches!(computed_output, Some(_)) { + panic!( + "invariant violation: we somehow matched multiple arms in case analysis" + ) + } computed_output = Some(output); } else { new_context.add_element( |