tessellate-core 0.9.0

use crate::ast::{
    BinaryOp, Declaration, Effect, ExpectedValue, Expr, ExprKind, FieldDecl, InvariantAssertion,
    InvariantDecl, InvariantQuantifier, Literal, NumericLiteral, RuleDecl, TypeRef,
};
use crate::compiler::{
    CompiledProgram, effective_decimal_range_bounds, effective_int_range_bounds, normalize_name,
};
use crate::engine::{
    DecisionStatus, Evaluation, Input, Query, constant_value, evaluate_condition, evaluate_query,
    resolve_rule_bindings,
};
use crate::solver::{SolverMetadata, SolverMode, SolverOutcome, solve_invariant};
use crate::value::{TruthValue, Value, parse_decimal};
use chrono::NaiveDate;
use rust_decimal::Decimal;
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};
use std::fmt::Write;

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct AnalysisOptions {
    /// Hard cap on concrete inputs or exact representatives evaluated per assertion.
    /// Symbolic solver queries do not consume this budget.
    pub max_evaluations: usize,
    /// Stop concrete exploration after collecting this many counterexamples.
    pub max_counterexamples: usize,
}

impl Default for AnalysisOptions {
    fn default() -> Self {
        Self {
            max_evaluations: 100_000,
            max_counterexamples: 3,
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum Completeness {
    /// Every value in every finite field range was enumerated.
    Exhaustive,
    /// One representative from every exact rule-threshold equivalence region was enumerated.
    ThresholdPartitioned,
    /// The embedded solver decided the exact quantifier-specific query in its supported theory.
    SolverExact,
    /// All generated boundary candidates were enumerated, but the domain was reduced.
    BoundarySampled,
    /// Verification stopped before covering the full plan, possibly after decisive evidence.
    Truncated,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum AnalysisVerdict {
    Passed,
    Failed,
    Inconclusive,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum CounterexampleKind {
    Undefined,
    Overdetermined,
    Unknown,
    Conflict,
    PropertyViolation,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Counterexample {
    pub invariant: String,
    pub kind: CounterexampleKind,
    pub input: Input,
    pub reason: String,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub evaluation: Option<Evaluation>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct InvariantAnalysis {
    pub invariant: String,
    /// The source-level quantifier whose proof result this record describes.
    #[serde(
        default = "default_invariant_quantifier",
        skip_serializing_if = "is_universal_quantifier"
    )]
    pub quantifier: InvariantQuantifier,
    pub verdict: AnalysisVerdict,
    pub evaluated: usize,
    pub planned_evaluations: usize,
    pub completeness: Completeness,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub solver: Option<SolverMetadata>,
    /// A concrete, evaluator-replayed assignment satisfying `assert some`.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub witness: Option<Input>,
    pub counterexamples: Vec<Counterexample>,
    #[serde(default, skip_serializing_if = "Vec::is_empty")]
    pub notes: Vec<String>,
}

const fn default_invariant_quantifier() -> InvariantQuantifier {
    InvariantQuantifier::All
}

// Serde's `skip_serializing_if` contract passes the field by reference even
// though this enum is `Copy`.
#[allow(clippy::trivially_copy_pass_by_ref)]
fn is_universal_quantifier(quantifier: &InvariantQuantifier) -> bool {
    *quantifier == InvariantQuantifier::All
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct StaticFinding {
    pub code: String,
    pub message: String,
}

#[derive(Clone, Debug, Default, Serialize, Deserialize)]
pub struct AnalysisReport {
    pub invariants: Vec<InvariantAnalysis>,
    pub findings: Vec<StaticFinding>,
}

impl AnalysisReport {
    #[must_use]
    pub fn success(&self) -> bool {
        !self.invariants.is_empty()
            && self
                .invariants
                .iter()
                .all(|invariant| invariant.verdict == AnalysisVerdict::Passed)
    }

    /// Render a concise, stable report for humans.
    ///
    /// Machine completeness names, solver metadata, and diagnostic notes remain
    /// available through serialization and the structured fields above.
    #[must_use]
    pub fn render_text(&self) -> String {
        let mut out = String::new();
        for finding in &self.findings {
            let _ = writeln!(out, "! {} · {}", finding.code, finding.message);
        }
        if !self.findings.is_empty() && !self.invariants.is_empty() {
            out.push('\n');
        }
        for (invariant_index, invariant) in self.invariants.iter().enumerate() {
            if invariant_index > 0 {
                out.push('\n');
            }
            let (marker, verdict) = match (invariant.quantifier, invariant.verdict) {
                (InvariantQuantifier::All, AnalysisVerdict::Passed) => {
                    ("✓", "proved for all inputs")
                }
                (InvariantQuantifier::Some, AnalysisVerdict::Passed) => {
                    ("✓", "satisfying input found")
                }
                (InvariantQuantifier::Some, AnalysisVerdict::Failed)
                    if invariant.counterexamples.is_empty() =>
                {
                    ("✗", "no satisfying input exists")
                }
                (_, AnalysisVerdict::Failed) if invariant.counterexamples.is_empty() => {
                    ("✗", "failed")
                }
                (_, AnalysisVerdict::Failed) => ("✗", "counterexample found"),
                (_, AnalysisVerdict::Inconclusive) => ("?", "inconclusive"),
            };
            let _ = writeln!(out, "{marker} {}", invariant.invariant);
            let _ = write!(out, "  {verdict}");
            let has_existential_witness = invariant.quantifier == InvariantQuantifier::Some
                && invariant.verdict == AnalysisVerdict::Passed
                && invariant.witness.is_some();
            if has_existential_witness && invariant.completeness != Completeness::SolverExact {
                let evaluations = format_count(invariant.evaluated);
                let noun = pluralized(invariant.evaluated, "evaluation", "evaluations");
                let _ = write!(out, " · after {evaluations} {noun}");
            } else {
                match invariant.completeness {
                    Completeness::Exhaustive => {
                        let combinations = format_count(invariant.planned_evaluations);
                        let noun = pluralized(
                            invariant.planned_evaluations,
                            "combination",
                            "combinations",
                        );
                        let _ = write!(out, " · all {combinations} {noun} checked");
                    }
                    Completeness::ThresholdPartitioned => {
                        let regions = format_count(invariant.evaluated);
                        let noun = pluralized(invariant.evaluated, "exact region", "exact regions");
                        let _ = write!(out, " · {regions} {noun} checked");
                    }
                    Completeness::SolverExact => {
                        out.push_str(" · exact solver");
                        if let Some(solver) = &invariant.solver {
                            let backend = if solver.backend.eq_ignore_ascii_case("z3") {
                                "Z3"
                            } else {
                                &solver.backend
                            };
                            let _ = write!(out, " ({backend})");
                        }
                    }
                    Completeness::BoundarySampled => {
                        let samples = format_count(invariant.evaluated);
                        let noun =
                            pluralized(invariant.evaluated, "boundary sample", "boundary samples");
                        let _ = write!(out, " · {samples} {noun} checked");
                        if invariant.verdict == AnalysisVerdict::Inconclusive {
                            out.push_str(" · not exhaustive");
                        }
                    }
                    Completeness::Truncated => {
                        let evaluated = format_count(invariant.evaluated);
                        if invariant.planned_evaluations == usize::MAX {
                            let _ = write!(out, " · {evaluated} evaluations · truncated");
                        } else {
                            let candidates = format_count(invariant.planned_evaluations);
                            let _ = write!(
                                out,
                                " · {evaluated} of {candidates} evaluations · truncated"
                            );
                        }
                    }
                }
            }
            out.push('\n');

            if invariant.verdict == AnalysisVerdict::Inconclusive
                || (invariant.verdict == AnalysisVerdict::Failed
                    && invariant.counterexamples.is_empty())
            {
                for note in invariant.notes.iter().filter(|note| human_note(note)) {
                    let _ = writeln!(out, "  reason · {note}");
                }
            }

            if let Some(witness) = &invariant.witness {
                out.push_str("\n  witness\n");
                for (binding, entity) in &witness.bindings {
                    let _ = writeln!(out, "    {binding}: {} {{", entity.entity);
                    for (field, value) in &entity.fields {
                        let _ = writeln!(out, "      {field}: {value},");
                    }
                    out.push_str("    }\n");
                }
            }

            for counterexample in &invariant.counterexamples {
                let kind = match counterexample.kind {
                    CounterexampleKind::Undefined => "undefined",
                    CounterexampleKind::Overdetermined => "overdetermined",
                    CounterexampleKind::Unknown => "unknown",
                    CounterexampleKind::Conflict => "conflict",
                    CounterexampleKind::PropertyViolation => "property violation",
                };
                let _ = writeln!(out, "\n  counterexample · {kind}");
                let _ = writeln!(out, "    reason · {}", counterexample.reason);
                for (binding, entity) in &counterexample.input.bindings {
                    let _ = writeln!(out, "    {binding}: {} {{", entity.entity);
                    for (field, value) in &entity.fields {
                        let _ = writeln!(out, "      {field}: {value},");
                    }
                    out.push_str("    }\n");
                }
                if let Some(evaluation) = &counterexample.evaluation {
                    for line in evaluation.render_text().lines() {
                        let _ = writeln!(out, "    {line}");
                    }
                }
            }
        }
        out
    }
}

fn pluralized<'a>(count: usize, singular: &'a str, plural: &'a str) -> &'a str {
    if count == 1 { singular } else { plural }
}

fn format_count(count: usize) -> String {
    let digits = count.to_string();
    let mut grouped = String::with_capacity(digits.len() + digits.len() / 3);
    for (index, digit) in digits.chars().enumerate() {
        if index > 0 && (digits.len() - index) % 3 == 0 {
            grouped.push(',');
        }
        grouped.push(digit);
    }
    grouped
}

fn human_note(note: &str) -> bool {
    note != "used an exact threshold partition: every representative stands for a region with identical relevant rule and assertion outcomes"
        && note
            != "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a counterexample is not a proof"
        && note
            != "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a satisfying input does not prove that none exists"
        && !note.starts_with("stopped at the configured evaluation limit of ")
}

#[derive(Clone, Debug)]
struct FieldDomain {
    name: String,
    values: Vec<Option<Value>>,
}

#[derive(Clone, Debug)]
struct QuantifiedDomain {
    binding: String,
    entity: String,
    fields: Vec<FieldDomain>,
}

/// Concrete exhaustive fields are stored in `Vec`s. Keep one maliciously large
/// `--max-evaluations` value from turning a valid analysis request into an OOM;
/// larger fields use the exact threshold quotient or the sampled fallback.
const MAX_MATERIALIZED_VALUES_PER_FIELD: usize = 1_000_000;

/// Exact representative enumeration is generally cheaper and more stable than
/// starting the SMT solver at this scale. Larger exact plans are retained as a
/// fallback, but the embedded solver gets the first chance to avoid thousands
/// of evaluator calls.
const EAGER_EXACT_ENUMERATION_LIMIT: usize = 1_024;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum DomainMode {
    Exhaustive,
    ThresholdPartitioned,
    BoundarySampled,
}

impl DomainMode {
    const fn completeness(self) -> Completeness {
        match self {
            Self::Exhaustive => Completeness::Exhaustive,
            Self::ThresholdPartitioned => Completeness::ThresholdPartitioned,
            Self::BoundarySampled => Completeness::BoundarySampled,
        }
    }
}

/// Analyze declared assertions with exact quotient enumeration, the embedded solver,
/// or a conservative deterministic boundary sample.
#[must_use]
pub fn analyze(
    program: &CompiledProgram,
    selected_invariant: Option<&str>,
    options: &AnalysisOptions,
) -> AnalysisReport {
    analyze_with_solver(program, selected_invariant, options, SolverMode::Auto)
}

/// Analyze assertions with compact exact enumeration first, then the embedded
/// solver, and only materialize a larger finite Cartesian product as a fallback.
#[must_use]
pub fn analyze_with_solver(
    program: &CompiledProgram,
    selected_invariant: Option<&str>,
    options: &AnalysisOptions,
    solver_mode: SolverMode,
) -> AnalysisReport {
    let mut invariants = program
        .ast()
        .declarations
        .iter()
        .filter_map(|declaration| match declaration {
            Declaration::Invariant(invariant)
                if selected_invariant.is_none_or(|selected| invariant.name.value == selected) =>
            {
                Some(invariant)
            }
            _ => None,
        })
        .collect::<Vec<_>>();
    invariants.sort_by(|left, right| left.name.value.cmp(&right.name.value));

    AnalysisReport {
        invariants: invariants
            .into_iter()
            .map(|invariant| analyze_invariant(program, invariant, options, solver_mode))
            .collect(),
        findings: static_findings(program),
    }
}

fn analyze_invariant(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    options: &AnalysisOptions,
    solver_mode: SolverMode,
) -> InvariantAnalysis {
    let mut quantified = Vec::new();
    for variable in &invariant.variables {
        let Some(entity) = program.entity(&variable.ty.value) else {
            return InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Failed,
                evaluated: 0,
                planned_evaluations: 0,
                completeness: Completeness::Truncated,
                solver: None,
                witness: None,
                counterexamples: Vec::new(),
                notes: vec![format!(
                    "assertion parameter type `{}` is not a record",
                    variable.ty.value
                )],
            };
        };
        quantified.push((variable, entity));
    }

    let exhaustive_size = quantified_domain_size(program, &quantified);
    let fields_materializable = quantified_fields_materializable(program, &quantified);
    let materialization_limited = exhaustive_size
        .is_some_and(|size| size <= options.max_evaluations && !fields_materializable);
    let exhaustive_within_limit = exhaustive_size
        .is_some_and(|size| size <= options.max_evaluations && fields_materializable);
    let eager_limit = options.max_evaluations.min(EAGER_EXACT_ENUMERATION_LIMIT);

    // An explicit `z3` request tries the solver before any concrete strategy.
    // If the exact fragment is unsupported, deterministic exact/sampled
    // fallbacks remain available and retain the reason in their notes.
    let mut requested_solver_note = if solver_mode == SolverMode::Z3 {
        match solver_exact_analysis(program, invariant, solver_mode) {
            Ok(analysis) => return analysis,
            Err(reason) => Some(reason),
        }
    } else {
        None
    };

    // Plan compact exact work before materializing a raw Cartesian product.
    // A compact threshold quotient is preferred in auto mode. If it is unavailable
    // or too large, try the solver before every raw Cartesian product.
    let threshold_plan = threshold_partition_domains(program, invariant);
    let (domains, domain_mode, partition_note) = match threshold_plan {
        Ok(domains) => {
            let threshold_size = planned_evaluation_count(&domains);
            if threshold_size.is_some_and(|size| size <= eager_limit) {
                (
                    domains,
                    DomainMode::ThresholdPartitioned,
                    Some(threshold_partition_note(requested_solver_note.as_deref())),
                )
            } else {
                let solver_note = if requested_solver_note.is_some() {
                    requested_solver_note.take()
                } else if solver_mode == SolverMode::Off {
                    None
                } else {
                    match solver_exact_analysis(program, invariant, solver_mode) {
                        Ok(analysis) => return analysis,
                        Err(reason) => Some(reason),
                    }
                };
                (
                    domains,
                    DomainMode::ThresholdPartitioned,
                    Some(threshold_partition_note(solver_note.as_deref())),
                )
            }
        }
        Err(threshold_reason) => {
            let solver_note = if requested_solver_note.is_some() {
                requested_solver_note.take()
            } else if solver_mode == SolverMode::Off {
                None
            } else {
                match solver_exact_analysis(program, invariant, solver_mode) {
                    Ok(analysis) => return analysis,
                    Err(reason) => Some(reason),
                }
            };
            let mut compact_note =
                format!("exact threshold partitioning was unavailable: {threshold_reason}");
            if let Some(solver_note) = solver_note {
                compact_note.push_str("; ");
                compact_note.push_str(&solver_note);
            }

            if exhaustive_within_limit {
                compact_note.push_str("; enumerated the complete finite domain instead");
                (
                    concrete_domains(program, &quantified, &BTreeSet::new(), true),
                    DomainMode::Exhaustive,
                    Some(compact_note),
                )
            } else {
                let constants = numeric_constants(program);
                (
                    concrete_domains(program, &quantified, &constants, false),
                    DomainMode::BoundarySampled,
                    Some(compact_note),
                )
            }
        }
    };
    let exact_planned_evaluations = planned_evaluation_count(&domains);
    let planned_evaluations = exact_planned_evaluations.unwrap_or(usize::MAX);
    let plan_count_overflowed = exact_planned_evaluations.is_none();
    let limit = planned_evaluations.min(options.max_evaluations);
    let mut evaluated = 0usize;
    let mut counterexamples = Vec::new();
    let mut existential_witness = None;
    let mut stopped_for_counterexamples = false;
    let mut stopped_for_witness = false;

    for ordinal in 0..limit {
        let input = input_at(ordinal, &domains);
        evaluated += 1;
        match invariant.quantifier {
            InvariantQuantifier::All => {
                if let Some(counterexample) = find_invariant_violation(program, invariant, &input) {
                    counterexamples.push(counterexample);
                    if counterexamples.len() >= options.max_counterexamples.max(1) {
                        stopped_for_counterexamples = ordinal + 1 < planned_evaluations;
                        break;
                    }
                }
            }
            InvariantQuantifier::Some => {
                if invariant_has_existential_witness(program, invariant, &input) {
                    stopped_for_witness = ordinal + 1 < planned_evaluations;
                    existential_witness = Some(input);
                    break;
                }
            }
        }
    }

    let completeness = if stopped_for_counterexamples
        || stopped_for_witness
        || plan_count_overflowed
        || planned_evaluations > options.max_evaluations
    {
        Completeness::Truncated
    } else {
        domain_mode.completeness()
    };
    let verdict = match invariant.quantifier {
        InvariantQuantifier::All => {
            if counterexamples.is_empty() {
                if matches!(
                    completeness,
                    Completeness::Exhaustive
                        | Completeness::ThresholdPartitioned
                        | Completeness::SolverExact
                ) {
                    AnalysisVerdict::Passed
                } else {
                    AnalysisVerdict::Inconclusive
                }
            } else {
                AnalysisVerdict::Failed
            }
        }
        InvariantQuantifier::Some if existential_witness.is_some() => AnalysisVerdict::Passed,
        InvariantQuantifier::Some
            if matches!(
                completeness,
                Completeness::Exhaustive | Completeness::ThresholdPartitioned
            ) =>
        {
            AnalysisVerdict::Failed
        }
        InvariantQuantifier::Some => AnalysisVerdict::Inconclusive,
    };
    let mut notes = Vec::new();
    if let Some(note) = partition_note {
        notes.push(note);
    }
    if materialization_limited {
        notes.push(format!(
            "concrete enumeration was not materialized because a field exceeds the internal safety cap of {MAX_MATERIALIZED_VALUES_PER_FIELD} values"
        ));
    }
    if domain_mode == DomainMode::BoundarySampled {
        notes.push(match invariant.quantifier {
            InvariantQuantifier::All => "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a counterexample is not a proof".into(),
            InvariantQuantifier::Some => "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a satisfying input does not prove that none exists".into(),
        });
    }
    if planned_evaluations > options.max_evaluations {
        notes.push(format!(
            "stopped at the configured evaluation limit of {}",
            options.max_evaluations
        ));
    }
    if plan_count_overflowed {
        notes.push("the planned evaluation count exceeds this platform's size limit".into());
    }
    if stopped_for_counterexamples {
        notes.push(format!(
            "stopped after {} counterexample(s)",
            options.max_counterexamples.max(1)
        ));
    }
    if stopped_for_witness {
        notes.push("stopped after finding the first satisfying input".into());
    }
    if invariant.quantifier == InvariantQuantifier::Some && verdict == AnalysisVerdict::Failed {
        notes.push(
            "every exact quantified assignment was checked, but none satisfied the assertion"
                .into(),
        );
    }

    InvariantAnalysis {
        invariant: invariant.name.value.clone(),
        quantifier: invariant.quantifier,
        verdict,
        evaluated,
        planned_evaluations,
        completeness,
        solver: None,
        witness: existential_witness,
        counterexamples,
        notes,
    }
}

fn concrete_domains(
    program: &CompiledProgram,
    quantified: &[(&crate::ast::Parameter, &crate::ast::EntityDecl)],
    constants: &BTreeSet<Decimal>,
    exhaustive: bool,
) -> Vec<QuantifiedDomain> {
    quantified
        .iter()
        .map(|(variable, entity)| QuantifiedDomain {
            binding: variable.name.value.clone(),
            entity: variable.ty.value.clone(),
            fields: entity
                .fields
                .iter()
                .map(|field| FieldDomain {
                    name: field.name.value.clone(),
                    values: field_values(program, field, constants, exhaustive),
                })
                .collect(),
        })
        .collect()
}

fn threshold_partition_note(solver_note: Option<&str>) -> String {
    let mut note = "used an exact threshold partition: every representative stands for a region with identical relevant rule and assertion outcomes".to_owned();
    if let Some(solver_note) = solver_note {
        note.push_str("; the solver attempt fell back to this exact partition: ");
        note.push_str(solver_note);
    }
    note
}

fn solver_exact_analysis(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    solver_mode: SolverMode,
) -> Result<InvariantAnalysis, String> {
    solver_outcome_analysis(
        program,
        invariant,
        solve_invariant(program, invariant, solver_mode),
    )
}

fn solver_outcome_analysis(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    outcome: SolverOutcome,
) -> Result<InvariantAnalysis, String> {
    match outcome {
        SolverOutcome::Proved(metadata) => {
            if invariant.quantifier != InvariantQuantifier::All {
                return Err("the solver returned a universal proof for `assert some`".into());
            }
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Passed,
                // No concrete input was evaluated. Z3 answered one symbolic query.
                evaluated: 0,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "the negated property is unsatisfiable in {} via {}",
                    metadata.logic, metadata.version
                )],
                solver: Some(metadata),
                witness: None,
                counterexamples: Vec::new(),
            })
        }
        SolverOutcome::Counterexample { input, metadata } => {
            if invariant.quantifier != InvariantQuantifier::All {
                return Err(
                    "the solver returned a universal counterexample for `assert some`".into(),
                );
            }
            let counterexample = replay_solver_counterexample(program, invariant, &input)?;
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Failed,
                // One SAT model was replayed, but no Cartesian product was enumerated.
                evaluated: 1,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "the {} model was replayed by the Tess evaluator",
                    metadata.logic
                )],
                solver: Some(metadata),
                witness: None,
                counterexamples: vec![counterexample],
            })
        }
        SolverOutcome::Witness { input, metadata } => {
            if invariant.quantifier != InvariantQuantifier::Some {
                return Err(
                    "the solver returned an existential witness for a universal `assert`".into(),
                );
            }
            check_invariant_witness(program, invariant, &input).map_err(|reason| {
                format!("the solver model did not reproduce a satisfying input: {reason}")
            })?;
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Passed,
                // One SAT model was replayed by the ordinary Tess evaluator.
                evaluated: 1,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "the satisfying {} model was replayed by the Tess evaluator",
                    metadata.logic
                )],
                solver: Some(metadata),
                witness: Some(input),
                counterexamples: Vec::new(),
            })
        }
        SolverOutcome::Refuted(metadata) => {
            if invariant.quantifier != InvariantQuantifier::Some {
                return Err(
                    "the solver returned an existential refutation for a universal `assert`".into(),
                );
            }
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Failed,
                evaluated: 0,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "no satisfying assignment exists in {} via {}",
                    metadata.logic, metadata.version
                )],
                solver: Some(metadata),
                witness: None,
                counterexamples: Vec::new(),
            })
        }
        SolverOutcome::Unavailable(reason) => Err(format!("embedded solver unavailable: {reason}")),
        SolverOutcome::Unsupported(reason) => {
            Err(format!("solver translation unavailable: {reason}"))
        }
        SolverOutcome::Unknown(reason) => {
            Err(format!("embedded solver was inconclusive: {reason}"))
        }
    }
}

fn replay_solver_counterexample(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> Result<Counterexample, String> {
    let Some(counterexample) = find_invariant_violation(program, invariant, input) else {
        return Err("the solver model did not reproduce a violation in the Tess evaluator".into());
    };
    if counterexample.kind == CounterexampleKind::Unknown {
        return Err(format!(
            "the solver model replay needed additional input: {}",
            counterexample.reason
        ));
    }
    Ok(counterexample)
}

fn planned_evaluation_count(domains: &[QuantifiedDomain]) -> Option<usize> {
    domains
        .iter()
        .flat_map(|domain| &domain.fields)
        .try_fold(1usize, |total, field| total.checked_mul(field.values.len()))
}

fn find_invariant_violation(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> Option<Counterexample> {
    match &invariant.assertion {
        InvariantAssertion::Cardinality {
            cardinality,
            decision,
            arguments,
            ..
        } => {
            let query = Query {
                decision: decision.value.clone(),
                arguments: arguments
                    .iter()
                    .filter_map(|argument| match &argument.kind {
                        ExprKind::Name(name) => Some(name.clone()),
                        _ => None,
                    })
                    .collect(),
            };
            let evaluation = match evaluate_query(program, input, &query) {
                Ok(evaluation) => evaluation,
                Err(error) => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: error.message,
                        evaluation: None,
                    });
                }
            };
            let failure = match (&evaluation.result.status, cardinality) {
                (DecisionStatus::Resolved { values }, crate::ast::Cardinality::ExactlyOne)
                    if values.len() == 1 =>
                {
                    None
                }
                (DecisionStatus::Resolved { values }, crate::ast::Cardinality::ZeroOrOne)
                    if values.len() <= 1 =>
                {
                    None
                }
                (DecisionStatus::Resolved { .. }, crate::ast::Cardinality::Many)
                | (
                    DecisionStatus::Undefined,
                    crate::ast::Cardinality::ZeroOrOne | crate::ast::Cardinality::Many,
                ) => None,
                (DecisionStatus::Undefined, _) => Some((
                    CounterexampleKind::Undefined,
                    "no decision candidate was produced".to_owned(),
                )),
                (DecisionStatus::Unknown { missing }, _) => Some((
                    CounterexampleKind::Unknown,
                    format!(
                        "the decision needs additional input: {}",
                        missing.join(", ")
                    ),
                )),
                (DecisionStatus::Conflict { values, reasons }, _) if values.len() > 1 => Some((
                    CounterexampleKind::Overdetermined,
                    format!(
                        "multiple values remain after explicit overrides: {}{}",
                        values
                            .iter()
                            .map(ToString::to_string)
                            .collect::<Vec<_>>()
                            .join(", "),
                        if reasons.is_empty() {
                            String::new()
                        } else {
                            format!(" ({})", reasons.join("; "))
                        }
                    ),
                )),
                (DecisionStatus::Conflict { reasons, .. }, _) => Some((
                    CounterexampleKind::Conflict,
                    if reasons.is_empty() {
                        "the decision has conflicting support".into()
                    } else {
                        reasons.join("; ")
                    },
                )),
                (DecisionStatus::Resolved { values }, _) if values.is_empty() => Some((
                    CounterexampleKind::Undefined,
                    "no decision candidate was produced".to_owned(),
                )),
                (DecisionStatus::Resolved { values }, _) => Some((
                    CounterexampleKind::Overdetermined,
                    format!("cardinality was violated by {} value(s)", values.len()),
                )),
            };
            failure.map(|(kind, reason)| Counterexample {
                invariant: invariant.name.value.clone(),
                kind,
                input: input.clone(),
                reason,
                evaluation: Some(evaluation),
            })
        }
        InvariantAssertion::Implication {
            condition,
            expectation,
            ..
        } => {
            let condition = evaluate_condition(
                program,
                input,
                invariant
                    .variables
                    .iter()
                    .map(|variable| (variable.name.value.clone(), variable.name.value.clone()))
                    .collect(),
                condition,
            );
            match condition.truth {
                TruthValue::False => return None,
                TruthValue::Unknown => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Unknown,
                        input: input.clone(),
                        reason: format!(
                            "property premise is unknown: {}",
                            condition.missing.join(", ")
                        ),
                        evaluation: None,
                    });
                }
                TruthValue::Conflict => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: condition.reasons.join("; "),
                        evaluation: None,
                    });
                }
                TruthValue::True => {}
            }
            let query = Query {
                decision: expectation.decision.value.clone(),
                arguments: expectation
                    .arguments
                    .iter()
                    .filter_map(|argument| match &argument.kind {
                        ExprKind::Name(name) => Some(name.clone()),
                        _ => None,
                    })
                    .collect(),
            };
            let evaluation = match evaluate_query(program, input, &query) {
                Ok(evaluation) => evaluation,
                Err(error) => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: error.message,
                        evaluation: None,
                    });
                }
            };
            let expected_type = program
                .decision(&expectation.decision.value)
                .map(|decision| &decision.return_type.value);
            let ExpectedValue::Scalar(expected_expression) = &expectation.expected else {
                return Some(Counterexample {
                    invariant: invariant.name.value.clone(),
                    kind: CounterexampleKind::Conflict,
                    input: input.clone(),
                    reason: "set expectations are valid only in concrete tests".to_owned(),
                    evaluation: Some(evaluation),
                });
            };
            let expected = match constant_value(program, expected_expression, expected_type) {
                Ok(expected) => expected,
                Err(error) => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: error,
                        evaluation: Some(evaluation),
                    });
                }
            };
            let failure = match &evaluation.result.status {
                DecisionStatus::Resolved { values } => {
                    let contains = values.contains(&expected);
                    let satisfied = match expectation.operator {
                        crate::ast::CompareOp::Equal => contains,
                        crate::ast::CompareOp::NotEqual => !contains,
                    };
                    (!satisfied).then_some((
                        CounterexampleKind::PropertyViolation,
                        format!(
                            "expected {} to satisfy the declared relation",
                            query.render()
                        ),
                    ))
                }
                DecisionStatus::Undefined => Some((
                    CounterexampleKind::PropertyViolation,
                    format!("{} is undefined", query.render()),
                )),
                DecisionStatus::Unknown { missing } => Some((
                    CounterexampleKind::Unknown,
                    format!(
                        "{} needs additional input: {}",
                        query.render(),
                        missing.join(", ")
                    ),
                )),
                DecisionStatus::Conflict { values, .. } if values.len() > 1 => Some((
                    CounterexampleKind::Overdetermined,
                    format!(
                        "{} has multiple values: {}",
                        query.render(),
                        values
                            .iter()
                            .map(ToString::to_string)
                            .collect::<Vec<_>>()
                            .join(", ")
                    ),
                )),
                DecisionStatus::Conflict { reasons, .. } => Some((
                    CounterexampleKind::Conflict,
                    if reasons.is_empty() {
                        format!("{} has conflicting support", query.render())
                    } else {
                        reasons.join("; ")
                    },
                )),
            };
            failure.map(|(kind, reason)| Counterexample {
                invariant: invariant.name.value.clone(),
                kind,
                input: input.clone(),
                reason,
                evaluation: Some(evaluation),
            })
        }
    }
}

fn invariant_has_existential_witness(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> bool {
    check_invariant_witness(program, invariant, input).is_ok()
}

fn check_invariant_witness(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> Result<(), String> {
    if let InvariantAssertion::Implication { condition, .. } = &invariant.assertion {
        let premise = evaluate_condition(
            program,
            input,
            invariant
                .variables
                .iter()
                .map(|variable| (variable.name.value.clone(), variable.name.value.clone()))
                .collect(),
            condition,
        );
        match premise.truth {
            TruthValue::True => {}
            TruthValue::False => {
                return Err("the existential property premise evaluates to X".into());
            }
            TruthValue::Unknown => {
                return Err(format!(
                    "the existential property premise needs additional input: {}",
                    premise.missing.join(", ")
                ));
            }
            TruthValue::Conflict => {
                return Err(if premise.reasons.is_empty() {
                    "the existential property premise has conflicting support".into()
                } else {
                    premise.reasons.join("; ")
                });
            }
        }
    }

    match find_invariant_violation(program, invariant, input) {
        None => Ok(()),
        Some(non_witness) => Err(non_witness.reason),
    }
}

/// Replay one concrete input against an assertion using the regular Tess
/// evaluator. This is kept crate-private so solver adapters cannot accidentally
/// bypass the evaluator's decision and conflict semantics.
pub(crate) fn replay_invariant_violation(
    program: &CompiledProgram,
    invariant_name: &str,
    input: &Input,
) -> Result<Option<Counterexample>, String> {
    let invariant = program
        .invariant(invariant_name)
        .ok_or_else(|| format!("unknown assertion `{invariant_name}`"))?;
    Ok(find_invariant_violation(program, invariant, input))
}

/// Replay one concrete input as evidence for an existential assertion.
///
/// Unlike ordinary implication, `assert some` with `P: Q` requires a witness
/// where both the premise and expectation hold. An `X` or indeterminate
/// premise is therefore not accepted as a vacuous witness.
pub(crate) fn replay_invariant_witness(
    program: &CompiledProgram,
    invariant_name: &str,
    input: &Input,
) -> Result<(), String> {
    let invariant = program
        .invariant(invariant_name)
        .ok_or_else(|| format!("unknown assertion `{invariant_name}`"))?;
    if invariant.quantifier != InvariantQuantifier::Some {
        return Err(format!(
            "assertion `{invariant_name}` is not declared with `assert some`"
        ));
    }
    check_invariant_witness(program, invariant, input)
}

#[derive(Clone, Debug)]
enum ThresholdFieldUse {
    Finite,
    Int { transitions: BTreeSet<i128> },
}

#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
struct QuantifiedField {
    binding: String,
    field: String,
}

#[derive(Default)]
struct ThresholdRequirements {
    fields: BTreeMap<QuantifiedField, ThresholdFieldUse>,
}

impl ThresholdRequirements {
    fn mark_finite(&mut self, field: QuantifiedField) {
        self.fields
            .entry(field)
            .or_insert(ThresholdFieldUse::Finite);
    }

    fn mark_int(&mut self, field: QuantifiedField, transitions: impl IntoIterator<Item = i128>) {
        match self
            .fields
            .entry(field)
            .or_insert_with(|| ThresholdFieldUse::Int {
                transitions: BTreeSet::new(),
            }) {
            ThresholdFieldUse::Int {
                transitions: existing,
            } => existing.extend(transitions),
            ThresholdFieldUse::Finite => {
                unreachable!("a compiled field cannot be both Int and finite-valued")
            }
        }
    }
}

struct ThresholdInspector<'a> {
    program: &'a CompiledProgram,
    binding_entities: BTreeMap<String, String>,
    requirements: ThresholdRequirements,
}

impl ThresholdInspector<'_> {
    fn inspect_condition(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<(), String> {
        if contains_call(expression) {
            return Err(
                "a relevant condition uses an `fn` call; only direct field predicates are partitionable"
                    .into(),
            );
        }
        if !depends_on_input(expression, receivers) {
            // A ground condition may be true, false, unknown, or conflicting, but its
            // outcome is identical for every input and therefore does not need a cut.
            return Ok(());
        }

        match &expression.kind {
            ExprKind::Field { .. } => {
                let Some((field_key, field_type)) =
                    self.direct_field(expression, receivers)?
                else {
                    return Err("a relevant condition contains an indirect field access".into());
                };
                if field_type != TypeRef::Bool {
                    return Err(format!(
                        "field `{}.{}` is used as a condition but is not Bool",
                        field_key.binding, field_key.field
                    ));
                }
                self.requirements.mark_finite(field_key);
                Ok(())
            }
            ExprKind::Unary {
                operator: crate::ast::UnaryOp::Not,
                operand,
            } => self.inspect_condition(operand, receivers),
            ExprKind::Binary {
                left,
                operator: BinaryOp::And | BinaryOp::Or,
                right,
            } => {
                self.inspect_condition(left, receivers)?;
                self.inspect_condition(right, receivers)
            }
            ExprKind::Binary {
                left,
                operator:
                    operator @ (BinaryOp::Equal
                    | BinaryOp::NotEqual
                    | BinaryOp::Greater
                    | BinaryOp::GreaterEqual
                    | BinaryOp::Less
                    | BinaryOp::LessEqual),
                right,
            } => self.inspect_comparison(left, *operator, right, receivers),
            ExprKind::Binary { .. } | ExprKind::Unary { .. } => Err(
                "a relevant condition applies arithmetic to an input field; only direct Int-field comparisons are partitionable"
                    .into(),
            ),
            ExprKind::Name(_) => Err(
                "a relevant condition depends directly on a record value instead of one of its fields"
                    .into(),
            ),
            ExprKind::Call { .. } => unreachable!("calls were rejected above"),
            ExprKind::Literal(_) => unreachable!("input-independent literals returned above"),
        }
    }

    fn inspect_comparison(
        &mut self,
        left: &Expr,
        operator: BinaryOp,
        right: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<(), String> {
        let left_field = self.direct_field(left, receivers)?;
        let right_field = self.direct_field(right, receivers)?;
        let (field_key, field_type, ground, normalized_operator) = match (left_field, right_field) {
            (Some(_), Some(_)) => {
                return Err(
                    "a relevant condition compares two input fields; cross-field predicates are not partitionable"
                        .into(),
                );
            }
            (Some((name, ty)), None) => (name, ty, right, operator),
            (None, Some((name, ty))) => (name, ty, left, reverse_comparison(operator)),
            (None, None) => {
                if depends_on_input(left, receivers) || depends_on_input(right, receivers) {
                    return Err(
                        "a relevant condition applies arithmetic to an input field; only direct Int-field comparisons are partitionable"
                            .into(),
                    );
                }
                return Ok(());
            }
        };
        if depends_on_input(ground, receivers) {
            return Err(
                "a relevant condition compares an input field with another input-dependent expression"
                    .into(),
            );
        }

        match field_type {
            TypeRef::Int => {
                let constant = ground_numeric_value(self.program, ground)?;
                let transitions = int_comparison_transitions(normalized_operator, constant)?;
                self.requirements.mark_int(field_key, transitions);
                Ok(())
            }
            TypeRef::Bool | TypeRef::Named(_) => {
                if !matches!(normalized_operator, BinaryOp::Equal | BinaryOp::NotEqual) {
                    return Err(format!(
                        "field `{}.{}` uses an unsupported ordered comparison",
                        field_key.binding, field_key.field
                    ));
                }
                constant_value(self.program, ground, Some(&field_type)).map_err(|error| {
                    format!(
                        "comparison with `{}.{}` is not ground: {error}",
                        field_key.binding, field_key.field
                    )
                })?;
                self.requirements.mark_finite(field_key);
                Ok(())
            }
            TypeRef::Decimal | TypeRef::String | TypeRef::Date | TypeRef::Duration => Err(format!(
                "relevant field `{}.{}` has type {}; threshold proofs currently support only Bool, enum, and Int fields",
                field_key.binding,
                field_key.field,
                type_ref_name(&field_type)
            )),
            TypeRef::Unknown => Err(format!(
                "relevant field `{}.{}` has an unresolved type",
                field_key.binding, field_key.field
            )),
        }
    }

    fn direct_field(
        &self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<Option<(QuantifiedField, TypeRef)>, String> {
        let ExprKind::Field {
            receiver, field, ..
        } = &expression.kind
        else {
            return Ok(None);
        };
        let ExprKind::Name(receiver_name) = &receiver.kind else {
            return Err("a relevant condition contains an indirect field receiver".into());
        };
        let receiver_name = normalize_name(receiver_name);
        let Some(binding) = receivers.get(&receiver_name) else {
            return Err(format!(
                "field access `{receiver_name}.{}` does not refer to an assertion record parameter",
                field.value
            ));
        };
        let entity_name = self.binding_entities.get(binding).ok_or_else(|| {
            format!("receiver `{receiver_name}` is not bound to an assertion record parameter")
        })?;
        let declaration = self
            .program
            .field(entity_name, &field.value)
            .ok_or_else(|| format!("unknown field `{}`", field.value))?;
        Ok(Some((
            QuantifiedField {
                binding: binding.clone(),
                field: normalize_name(&field.value),
            },
            declaration.ty.clone(),
        )))
    }

    fn require_constant(
        &self,
        expression: &Expr,
        expected: &TypeRef,
        receivers: &BTreeMap<String, String>,
        context: &str,
    ) -> Result<(), String> {
        if contains_call(expression) {
            return Err(format!(
                "{context} uses an `fn` call instead of an input-independent constant"
            ));
        }
        if depends_on_input(expression, receivers) {
            return Err(format!("{context} depends on an input value"));
        }
        constant_value(self.program, expression, Some(expected))
            .map(|_| ())
            .map_err(|error| format!("{context} is not a valid constant: {error}"))
    }
}

/// Construct an exact finite quotient of the concrete input domain.
///
/// Eligibility guarantees that every input-dependent atom is either a finite
/// Bool/enum observation or a direct `Int-field op ground-number` comparison.
/// Such an Int atom changes truth value only at the transition cuts recorded
/// below. Relevant effects and expectations are constant, and no relevant rule
/// reads an unused field. Consequently every concrete input maps to exactly one
/// representative whose relevant rule conditions, override activity, candidate
/// values, and assertion premise are identical. Enumerating all representatives is
/// therefore a proof, not boundary sampling.
fn threshold_partition_domains(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
) -> Result<Vec<QuantifiedDomain>, String> {
    let (decision_name, query_arguments) = match &invariant.assertion {
        InvariantAssertion::Cardinality {
            decision,
            arguments,
            ..
        } => (&decision.value, arguments.as_slice()),
        InvariantAssertion::Implication { expectation, .. } => (
            &expectation.decision.value,
            expectation.arguments.as_slice(),
        ),
    };
    let binding_entities = invariant
        .variables
        .iter()
        .map(|variable| {
            (
                normalize_name(&variable.name.value),
                normalize_name(&variable.ty.value),
            )
        })
        .collect::<BTreeMap<_, _>>();
    let query_bindings = query_arguments
        .iter()
        .map(|argument| {
            let ExprKind::Name(name) = &argument.kind else {
                return Err(
                    "the assertion decision must be called directly with record parameters"
                        .to_owned(),
                );
            };
            let name = normalize_name(name);
            if !binding_entities.contains_key(&name) {
                return Err(format!(
                    "decision argument `{name}` is not an assertion record parameter"
                ));
            }
            Ok(name)
        })
        .collect::<Result<Vec<_>, String>>()?;
    let decision = program
        .decision(decision_name)
        .ok_or_else(|| format!("unknown decision `{decision_name}`"))?;
    if decision.parameters.len() != query_bindings.len() {
        return Err("the assertion decision argument count is inconsistent".into());
    }
    for (parameter, binding) in decision.parameters.iter().zip(&query_bindings) {
        if binding_entities.get(binding) != Some(&normalize_name(&parameter.ty.value)) {
            return Err(format!(
                "decision argument `{binding}` has an incompatible assertion record type"
            ));
        }
    }

    let normalized_decision = normalize_name(decision_name);
    let query = Query {
        decision: normalized_decision.clone(),
        arguments: query_bindings,
    };
    let candidate_rule_names = program
        .rules()
        .iter()
        .filter(|(_, rule)| rule_directly_decides(rule, &normalized_decision))
        .map(|(name, _)| name.clone())
        .collect::<BTreeSet<_>>();
    let relevant_rules = program
        .rules()
        .iter()
        .filter(|(name, rule)| {
            candidate_rule_names.contains(*name)
                || rule.override_targets().any(|(target, _)| {
                    candidate_rule_names.contains(&normalize_name(&target.value))
                })
        })
        .map(|(_, rule)| rule)
        .collect::<Vec<_>>();

    let mut inspector = ThresholdInspector {
        program,
        binding_entities: binding_entities.clone(),
        requirements: ThresholdRequirements::default(),
    };
    let invariant_receivers = binding_entities
        .keys()
        .map(|binding| (binding.clone(), binding.clone()))
        .collect::<BTreeMap<_, _>>();
    if let InvariantAssertion::Implication {
        condition,
        expectation,
        ..
    } = &invariant.assertion
    {
        inspector.inspect_condition(condition, &invariant_receivers)?;
        let ExpectedValue::Scalar(expected_expression) = &expectation.expected else {
            return Err("set expectations are outside assertion analysis".to_owned());
        };
        inspector.require_constant(
            expected_expression,
            &decision.return_type.value,
            &invariant_receivers,
            "the assertion expectation",
        )?;
    }

    for rule in relevant_rules {
        inspect_relevant_rule(&mut inspector, rule, decision, &query, &binding_entities)?;
    }

    build_threshold_domains(program, &invariant.variables, &inspector.requirements)
}

fn inspect_relevant_rule(
    inspector: &mut ThresholdInspector<'_>,
    rule: &RuleDecl,
    decision: &crate::ast::DecisionDecl,
    query: &Query,
    binding_entities: &BTreeMap<String, String>,
) -> Result<(), String> {
    let parameter_names = rule
        .parameters
        .iter()
        .map(|parameter| normalize_name(&parameter.name.value))
        .collect::<BTreeSet<_>>();
    if let Effect::Decide {
        decision: target,
        arguments,
        ..
    } = &rule.effect
    {
        if normalize_name(&target.value) == query.decision
            && (arguments.len() != query.arguments.len()
                || arguments.iter().any(|argument| {
                    !matches!(&argument.kind, ExprKind::Name(name)
                        if parameter_names.contains(&normalize_name(name)))
                }))
        {
            return Err(format!(
                "relevant rule `{}` uses a dynamic decision argument",
                rule.name.value
            ));
        }
    }
    let receivers = resolve_rule_bindings(rule, decision, query, binding_entities)
        .map_err(|reason| format!("relevant rule `{}` {reason}", rule.name.value))?;
    inspector.inspect_condition(&rule.condition, &receivers)?;

    if let Effect::Decide {
        decision: target,
        arguments,
        value,
        ..
    } = &rule.effect
    {
        if normalize_name(&target.value) == query.decision {
            if arguments.len() != decision.parameters.len() {
                return Err(format!(
                    "relevant rule `{}` uses a dynamic decision argument",
                    rule.name.value
                ));
            }
            inspector.require_constant(
                value,
                &decision.return_type.value,
                &receivers,
                &format!("candidate value in rule `{}`", rule.name.value),
            )?;
        }
    }
    Ok(())
}

fn rule_directly_decides(rule: &RuleDecl, decision: &str) -> bool {
    matches!(&rule.effect, Effect::Decide { decision: target, .. }
            if normalize_name(&target.value) == decision)
}

fn contains_call(expression: &Expr) -> bool {
    match &expression.kind {
        ExprKind::Call { .. } => true,
        ExprKind::Field { receiver, .. } => contains_call(receiver),
        ExprKind::Unary { operand, .. } => contains_call(operand),
        ExprKind::Binary { left, right, .. } => contains_call(left) || contains_call(right),
        ExprKind::Literal(_) | ExprKind::Name(_) => false,
    }
}

fn depends_on_input(expression: &Expr, receivers: &BTreeMap<String, String>) -> bool {
    match &expression.kind {
        ExprKind::Field { .. } => true,
        ExprKind::Name(name) => receivers.contains_key(&normalize_name(name)),
        ExprKind::Call { arguments, .. } => arguments
            .iter()
            .any(|argument| depends_on_input(argument, receivers)),
        ExprKind::Unary { operand, .. } => depends_on_input(operand, receivers),
        ExprKind::Binary { left, right, .. } => {
            depends_on_input(left, receivers) || depends_on_input(right, receivers)
        }
        ExprKind::Literal(_) => false,
    }
}

fn ground_numeric_value(program: &CompiledProgram, expression: &Expr) -> Result<Decimal, String> {
    match constant_value(program, expression, Some(&TypeRef::Decimal))? {
        Value::Int(value) => Ok(Decimal::from(value)),
        Value::Decimal(value) => Ok(value),
        value => Err(format!("expected a ground numeric value, found {value}")),
    }
}

const fn reverse_comparison(operator: BinaryOp) -> BinaryOp {
    match operator {
        BinaryOp::Greater => BinaryOp::Less,
        BinaryOp::GreaterEqual => BinaryOp::LessEqual,
        BinaryOp::Less => BinaryOp::Greater,
        BinaryOp::LessEqual => BinaryOp::GreaterEqual,
        BinaryOp::Equal
        | BinaryOp::NotEqual
        | BinaryOp::And
        | BinaryOp::Or
        | BinaryOp::Add
        | BinaryOp::Subtract
        | BinaryOp::Multiply
        | BinaryOp::Divide => operator,
    }
}

fn int_comparison_transitions(operator: BinaryOp, constant: Decimal) -> Result<Vec<i128>, String> {
    let floor = i128::try_from(constant.floor())
        .map_err(|_| format!("numeric threshold `{constant}` is outside the supported range"))?;
    let ceil = i128::try_from(constant.ceil())
        .map_err(|_| format!("numeric threshold `{constant}` is outside the supported range"))?;
    let transitions = match operator {
        BinaryOp::Less | BinaryOp::GreaterEqual => vec![ceil],
        BinaryOp::LessEqual | BinaryOp::Greater => vec![floor + 1],
        BinaryOp::Equal | BinaryOp::NotEqual if constant.fract().is_zero() => {
            vec![floor, floor + 1]
        }
        BinaryOp::Equal | BinaryOp::NotEqual => Vec::new(),
        _ => return Err("expected a comparison operator".into()),
    };
    Ok(transitions)
}

fn build_threshold_domains(
    program: &CompiledProgram,
    variables: &[crate::ast::Parameter],
    requirements: &ThresholdRequirements,
) -> Result<Vec<QuantifiedDomain>, String> {
    variables
        .iter()
        .map(|variable| {
            let binding = normalize_name(&variable.name.value);
            let entity = program
                .entity(&variable.ty.value)
                .ok_or_else(|| format!("unknown assertion record `{}`", variable.ty.value))?;
            let fields = entity
                .fields
                .iter()
                .map(|field| {
                    let key = QuantifiedField {
                        binding: binding.clone(),
                        field: normalize_name(&field.name.value),
                    };
                    let values = match requirements.fields.get(&key) {
                        Some(ThresholdFieldUse::Finite) => finite_partition_values(program, field)?,
                        Some(ThresholdFieldUse::Int { transitions }) => {
                            int_partition_values(field, transitions)?
                        }
                        None => vec![unused_field_representative(program, field)?],
                    };
                    Ok(FieldDomain {
                        name: field.name.value.clone(),
                        values,
                    })
                })
                .collect::<Result<Vec<_>, String>>()?;
            Ok(QuantifiedDomain {
                binding: variable.name.value.clone(),
                entity: variable.ty.value.clone(),
                fields,
            })
        })
        .collect()
}

fn finite_partition_values(
    program: &CompiledProgram,
    field: &FieldDecl,
) -> Result<Vec<Option<Value>>, String> {
    let values = match &field.ty {
        TypeRef::Bool => vec![Value::Bool(false), Value::Bool(true)],
        TypeRef::Named(name) => program
            .enum_decl(name)
            .map_or_else(Vec::new, |declaration| {
                declaration
                    .variants
                    .iter()
                    .map(|variant| Value::Enum {
                        type_name: name.clone(),
                        variant: variant.value.clone(),
                    })
                    .collect()
            }),
        _ => {
            return Err(format!(
                "field `{}` is not a finite Bool or enum field",
                field.name.value
            ));
        }
    };
    let mut values = values.into_iter().map(Some).collect::<Vec<_>>();
    if field.optional {
        values.insert(0, None);
    }
    if values.is_empty() {
        return Err(format!(
            "field `{}` has no representable values",
            field.name.value
        ));
    }
    Ok(values)
}

fn int_partition_values(
    field: &FieldDecl,
    transitions: &BTreeSet<i128>,
) -> Result<Vec<Option<Value>>, String> {
    let (start, end) = int_field_bounds(field)?;
    let lower = i128::from(start);
    let upper_exclusive = i128::from(end) + 1;
    let mut cuts = BTreeSet::from([lower, upper_exclusive]);
    cuts.extend(
        transitions
            .iter()
            .copied()
            .filter(|cut| lower < *cut && *cut < upper_exclusive),
    );
    let ordered = cuts.into_iter().collect::<Vec<_>>();
    let mut values = ordered
        .windows(2)
        .map(|window| {
            i64::try_from(window[0])
                .map(Value::Int)
                .map(Some)
                .map_err(|_| "integer partition representative is outside i64".to_owned())
        })
        .collect::<Result<Vec<_>, _>>()?;
    if field.optional {
        values.insert(0, None);
    }
    Ok(values)
}

fn int_field_bounds(field: &FieldDecl) -> Result<(i64, i64), String> {
    let Some(range) = &field.range else {
        return Ok((i64::MIN, i64::MAX));
    };
    effective_int_range_bounds(range).ok_or_else(|| {
        format!(
            "Int field `{}` has invalid or empty range bounds",
            field.name.value
        )
    })
}

fn unused_field_representative(
    program: &CompiledProgram,
    field: &FieldDecl,
) -> Result<Option<Value>, String> {
    if field.optional {
        return Ok(None);
    }
    let value = match &field.ty {
        TypeRef::Bool => Value::Bool(false),
        TypeRef::Int => Value::Int(
            int_field_bounds(field)?
                .0
                .max(0)
                .min(int_field_bounds(field)?.1),
        ),
        TypeRef::Decimal => {
            let value = field
                .range
                .as_ref()
                .and_then(effective_decimal_range_bounds)
                .map_or(Decimal::ZERO, |(start, _)| start);
            Value::decimal(value)
        }
        TypeRef::String => Value::String(String::new()),
        TypeRef::Date => {
            Value::Date(NaiveDate::from_ymd_opt(1970, 1, 1).expect("valid epoch date"))
        }
        TypeRef::Duration => Value::Duration(0),
        TypeRef::Named(name) => {
            let variant = program
                .enum_decl(name)
                .and_then(|declaration| declaration.variants.first())
                .ok_or_else(|| format!("field `{}` has no enum values", field.name.value))?;
            Value::Enum {
                type_name: name.clone(),
                variant: variant.value.clone(),
            }
        }
        TypeRef::Unknown => {
            return Err(format!(
                "field `{}` has an unresolved type",
                field.name.value
            ));
        }
    };
    Ok(Some(value))
}

const fn type_ref_name(value: &TypeRef) -> &'static str {
    match value {
        TypeRef::Bool => "Bool",
        TypeRef::Int => "Int",
        TypeRef::Decimal => "Decimal",
        TypeRef::String => "String",
        TypeRef::Date => "Date",
        TypeRef::Duration => "Duration",
        TypeRef::Named(_) => "enum",
        TypeRef::Unknown => "unknown",
    }
}

fn input_at(mut ordinal: usize, domains: &[QuantifiedDomain]) -> Input {
    let field_count = domains.iter().map(|domain| domain.fields.len()).sum();
    let mut indices = vec![0; field_count];
    let fields = domains
        .iter()
        .flat_map(|domain| &domain.fields)
        .collect::<Vec<_>>();
    for (index, field) in fields.iter().enumerate().rev() {
        indices[index] = ordinal % field.values.len();
        ordinal /= field.values.len();
    }
    let mut input = Input::new();
    let mut index = 0;
    for domain in domains {
        let mut values = BTreeMap::new();
        for field in &domain.fields {
            if let Some(value) = &field.values[indices[index]] {
                values.insert(field.name.clone(), value.clone());
            }
            index += 1;
        }
        input.insert(&domain.binding, &domain.entity, values);
    }
    input
}

fn quantified_domain_size(
    program: &CompiledProgram,
    quantified: &[(&crate::ast::Parameter, &crate::ast::EntityDecl)],
) -> Option<usize> {
    quantified.iter().try_fold(1usize, |total, (_, entity)| {
        total.checked_mul(finite_domain_size(program, entity)?)
    })
}

fn quantified_fields_materializable(
    program: &CompiledProgram,
    quantified: &[(&crate::ast::Parameter, &crate::ast::EntityDecl)],
) -> bool {
    quantified
        .iter()
        .all(|(_, entity)| concrete_fields_materializable(program, entity))
}

fn finite_domain_size(program: &CompiledProgram, entity: &crate::ast::EntityDecl) -> Option<usize> {
    entity.fields.iter().try_fold(1usize, |total, field| {
        let base = if let Some(values) = declared_domain_values(program, field) {
            values.len()
        } else {
            match &field.ty {
                TypeRef::Bool => 2,
                TypeRef::Int => {
                    let range = field.range.as_ref()?;
                    let (start, end) = effective_int_range_bounds(range)?;
                    let width = i128::from(end) - i128::from(start) + 1;
                    usize::try_from(width).ok()?
                }
                TypeRef::Named(name) => program.enum_decl(name)?.variants.len(),
                TypeRef::Decimal
                | TypeRef::String
                | TypeRef::Date
                | TypeRef::Duration
                | TypeRef::Unknown => return None,
            }
        };
        total.checked_mul(base.checked_add(usize::from(field.optional))?)
    })
}

fn concrete_fields_materializable(
    program: &CompiledProgram,
    entity: &crate::ast::EntityDecl,
) -> bool {
    entity.fields.iter().all(|field| {
        let base = if let Some(values) = declared_domain_values(program, field) {
            values.len()
        } else {
            match &field.ty {
                TypeRef::Bool => 2,
                TypeRef::Int => {
                    let Some(range) = &field.range else {
                        return false;
                    };
                    let Some((start, end)) = effective_int_range_bounds(range) else {
                        return false;
                    };
                    let width = i128::from(end) - i128::from(start) + 1;
                    let Ok(width) = usize::try_from(width) else {
                        return false;
                    };
                    width
                }
                TypeRef::Named(name) => {
                    let Some(declaration) = program.enum_decl(name) else {
                        return false;
                    };
                    declaration.variants.len()
                }
                TypeRef::Decimal
                | TypeRef::String
                | TypeRef::Date
                | TypeRef::Duration
                | TypeRef::Unknown => return false,
            }
        };
        base.checked_add(usize::from(field.optional))
            .is_some_and(|size| size <= MAX_MATERIALIZED_VALUES_PER_FIELD)
    })
}

fn field_values(
    program: &CompiledProgram,
    field: &crate::ast::FieldDecl,
    constants: &BTreeSet<Decimal>,
    exhaustive: bool,
) -> Vec<Option<Value>> {
    let mut values = if let Some(values) = declared_domain_values(program, field) {
        values
    } else {
        match &field.ty {
            TypeRef::Bool => vec![Value::Bool(false), Value::Bool(true)],
            TypeRef::Int => integer_values(field, constants, exhaustive),
            TypeRef::Decimal => decimal_values(field, constants),
            TypeRef::String => vec![Value::String(String::new())],
            TypeRef::Date => vec![Value::Date(
                NaiveDate::from_ymd_opt(1970, 1, 1).expect("valid epoch date"),
            )],
            TypeRef::Duration => vec![Value::Duration(0)],
            TypeRef::Named(name) => program.enum_decl(name).map_or_else(Vec::new, |value| {
                value
                    .variants
                    .iter()
                    .map(|variant| Value::Enum {
                        type_name: name.clone(),
                        variant: variant.value.clone(),
                    })
                    .collect()
            }),
            TypeRef::Unknown => Vec::new(),
        }
    };
    let mut seen = BTreeSet::new();
    values.retain(|value| seen.insert(value.clone()));
    let mut optional = values.into_iter().map(Some).collect::<Vec<_>>();
    if field.optional {
        optional.insert(0, None);
    }
    if optional.is_empty() {
        optional.push(None);
    }
    optional
}

fn declared_domain_values(
    program: &CompiledProgram,
    field: &crate::ast::FieldDecl,
) -> Option<Vec<Value>> {
    let domain = field.domain.as_ref()?;
    domain
        .values
        .iter()
        .map(|expression| constant_value(program, expression, Some(&field.ty)).ok())
        .collect()
}

fn integer_values(
    field: &crate::ast::FieldDecl,
    constants: &BTreeSet<Decimal>,
    exhaustive: bool,
) -> Vec<Value> {
    let range = field.range.as_ref().and_then(effective_int_range_bounds);
    if exhaustive {
        if let Some((start, end)) = range {
            return (start..=end).map(Value::Int).collect();
        }
    }
    if range.is_none() {
        let mut candidates = BTreeSet::from([-1, 0, 1]);
        for constant in constants {
            if constant.fract().is_zero() {
                if let Ok(value) = i64::try_from(constant.trunc()) {
                    candidates.extend([value.saturating_sub(1), value, value.saturating_add(1)]);
                }
            }
        }
        return candidates.into_iter().map(Value::Int).collect();
    }
    let (start, end) = range.expect("range was checked above");
    let mut candidates = BTreeSet::from([start, end]);
    if start < end {
        candidates.insert(start.saturating_add(1));
        candidates.insert(end.saturating_sub(1));
    }
    for base in [-1, 0, 1] {
        if (start..=end).contains(&base) {
            candidates.insert(base);
        }
    }
    for constant in constants {
        if constant.fract().is_zero() {
            if let Ok(value) = i64::try_from(constant.trunc()) {
                for candidate in [value.saturating_sub(1), value, value.saturating_add(1)] {
                    if (start..=end).contains(&candidate) {
                        candidates.insert(candidate);
                    }
                }
            }
        }
    }
    candidates.into_iter().map(Value::Int).collect()
}

fn decimal_values(field: &crate::ast::FieldDecl, constants: &BTreeSet<Decimal>) -> Vec<Value> {
    let range = field
        .range
        .as_ref()
        .and_then(effective_decimal_range_bounds);
    let epsilon = Decimal::new(1, 3);
    if range.is_none() {
        let mut candidates = BTreeSet::from([Decimal::NEGATIVE_ONE, Decimal::ZERO, Decimal::ONE]);
        for constant in constants {
            candidates.insert(*constant);
            if let Some(value) = constant.checked_sub(epsilon) {
                candidates.insert(value);
            }
            if let Some(value) = constant.checked_add(epsilon) {
                candidates.insert(value);
            }
        }
        return candidates
            .into_iter()
            .map(|value| Value::decimal(value.normalize()))
            .collect();
    }
    let (start, end) = range.expect("range was checked above");
    let mut candidates = BTreeSet::from([start, end]);
    for value in [Decimal::NEGATIVE_ONE, Decimal::ZERO, Decimal::ONE] {
        if value >= start && value <= end {
            candidates.insert(value);
        }
    }
    for constant in constants {
        let neighbors = [
            constant.checked_sub(epsilon),
            Some(*constant),
            constant.checked_add(epsilon),
        ];
        for value in neighbors.into_iter().flatten() {
            if value >= start && value <= end {
                candidates.insert(value.normalize());
            }
        }
    }
    candidates.into_iter().map(Value::decimal).collect()
}

fn numeric_decimal(literal: &NumericLiteral) -> Option<Decimal> {
    match literal {
        NumericLiteral::Int(value) => Some(Decimal::from(*value)),
        NumericLiteral::Decimal(value) => parse_decimal(value).ok(),
    }
}

fn numeric_constants(program: &CompiledProgram) -> BTreeSet<Decimal> {
    let mut constants = BTreeSet::new();
    for declaration in &program.ast().declarations {
        match declaration {
            Declaration::Derive(value) => collect_expr_numbers(&value.expression, &mut constants),
            Declaration::Rule(value) => {
                collect_expr_numbers(&value.condition, &mut constants);
                if let crate::ast::Effect::Decide {
                    arguments, value, ..
                } = &value.effect
                {
                    for argument in arguments {
                        collect_expr_numbers(argument, &mut constants);
                    }
                    collect_expr_numbers(value, &mut constants);
                }
            }
            Declaration::Fragment(value) => {
                for derive in &value.derives {
                    collect_expr_numbers(&derive.expression, &mut constants);
                }
                for rule in &value.rules {
                    collect_expr_numbers(&rule.condition, &mut constants);
                    if let crate::ast::Effect::Decide {
                        arguments, value, ..
                    } = &rule.effect
                    {
                        for argument in arguments {
                            collect_expr_numbers(argument, &mut constants);
                        }
                        collect_expr_numbers(value, &mut constants);
                    }
                }
            }
            // Concrete regression tests must not enlarge the analyzer's abstract
            // domain. Only rule and property boundaries influence exploration.
            Declaration::Case(_)
            | Declaration::Fixture(_)
            | Declaration::Enum(_)
            | Declaration::Entity(_)
            | Declaration::Decision(_) => {}
            Declaration::Invariant(value) => match &value.assertion {
                InvariantAssertion::Cardinality { arguments, .. } => {
                    for argument in arguments {
                        collect_expr_numbers(argument, &mut constants);
                    }
                }
                InvariantAssertion::Implication {
                    condition,
                    expectation,
                    ..
                } => {
                    collect_expr_numbers(condition, &mut constants);
                    for expected in expectation.expected.expressions() {
                        collect_expr_numbers(expected, &mut constants);
                    }
                }
            },
        }
    }
    constants
}

fn collect_expr_numbers(expression: &Expr, constants: &mut BTreeSet<Decimal>) {
    match &expression.kind {
        ExprKind::Literal(Literal::Number(value)) => {
            if let Some(value) = numeric_decimal(value) {
                constants.insert(value);
            }
        }
        ExprKind::Field { receiver, .. } => collect_expr_numbers(receiver, constants),
        ExprKind::Call { arguments, .. } => {
            for argument in arguments {
                collect_expr_numbers(argument, constants);
            }
        }
        ExprKind::Unary { operand, .. } => collect_expr_numbers(operand, constants),
        ExprKind::Binary { left, right, .. } => {
            collect_expr_numbers(left, constants);
            collect_expr_numbers(right, constants);
        }
        ExprKind::Literal(_) | ExprKind::Name(_) => {}
    }
}

fn static_findings(program: &CompiledProgram) -> Vec<StaticFinding> {
    let mut produced: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
    let decision_enums = program
        .decisions()
        .values()
        .filter_map(|decision| match &decision.return_type.value {
            TypeRef::Named(name) if program.enum_decl(name).is_some() => Some(name.clone()),
            _ => None,
        })
        .collect::<BTreeSet<_>>();
    let mut dynamic = BTreeSet::new();
    for rule in program.rules().values() {
        if let crate::ast::Effect::Decide {
            decision, value, ..
        } = &rule.effect
        {
            let Some(decision_decl) = program.decision(&decision.value) else {
                continue;
            };
            let TypeRef::Named(enum_name) = &decision_decl.return_type.value else {
                continue;
            };
            if let ExprKind::Name(variant) = &value.kind {
                let variant = variant.rsplit('.').next().unwrap_or(variant);
                produced
                    .entry(enum_name.clone())
                    .or_default()
                    .insert(normalize_name(variant));
            } else {
                dynamic.insert(enum_name.clone());
            }
        }
    }
    let mut findings = Vec::new();
    for name in decision_enums {
        if dynamic.contains(&name) {
            continue;
        }
        let enum_decl = &program.enums()[&name];
        let values = produced.get(&name);
        for variant in &enum_decl.variants {
            if values.is_none_or(|values| !values.contains(&normalize_name(&variant.value))) {
                findings.push(StaticFinding {
                    code: "W2001".into(),
                    message: format!(
                        "enum value `{}.{}` is never produced by a decision rule",
                        name, variant.value
                    ),
                });
            }
        }
    }
    findings.sort_by(|left, right| (&left.code, &left.message).cmp(&(&right.code, &right.message)));
    findings
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::ast::{EntityDecl, FieldDecl, RangeConstraint};
    use crate::source::{SourceFile, Span, Spanned};

    fn compile_text(source: &str) -> CompiledProgram {
        let output = crate::compile_source(SourceFile::new("analysis.tes", source));
        assert!(
            !output.has_errors(),
            "{}",
            output
                .diagnostics
                .iter()
                .map(|diagnostic| diagnostic.message.as_str())
                .collect::<Vec<_>>()
                .join("; ")
        );
        output.program.expect("compiled program")
    }

    #[test]
    fn numeric_constants_include_functions_nested_in_fragments() {
        let program = compile_text(
            r"law.formula:
    The fixed multiplier comes from this source.

    fn multiplier Decimal:
        12.5
",
        );
        assert!(numeric_constants(&program).contains(&Decimal::new(125, 1)));
    }

    #[test]
    fn static_findings_include_rules_nested_in_fragments() {
        let program = compile_text(
            r"enum Result:
    Yes
    No

record Request:
    enabled: Bool


policy.result:
    Enabled requests are accepted; other requests are rejected.

    rule yes(request Request):
        request.enabled: result(request) = Yes

    rule no(request Request):
        request.enabled X: result(request) = No
",
        );
        assert!(static_findings(&program).is_empty());
    }

    #[test]
    fn static_findings_match_canonical_inferred_enum_variants() {
        let program = compile_text(
            r"enum Result:
    Yes
    No

record Request:
    enabled: Bool

rule yes(request Request):
    request.enabled: result(request) = Result.Yes

rule no(request Request):
    request.enabled X: result(request) = Result.No
",
        );
        let produced = program
            .rules()
            .values()
            .filter_map(|rule| match &rule.effect {
                Effect::Decide { value, .. } => match &value.kind {
                    ExprKind::Name(name) => Some(name.as_str()),
                    _ => None,
                },
                Effect::Override { .. } | Effect::Invalid { .. } => None,
            })
            .collect::<BTreeSet<_>>();
        assert_eq!(produced, BTreeSet::from(["Result.No", "Result.Yes"]));
        assert!(static_findings(&program).is_empty());
    }

    fn analyze_text(source: &str, max_evaluations: usize) -> InvariantAnalysis {
        let report = analyze_with_solver(
            &compile_text(source),
            Some("total"),
            &AnalysisOptions {
                max_evaluations,
                max_counterexamples: 3,
            },
            SolverMode::Off,
        );
        report
            .invariants
            .into_iter()
            .next()
            .expect("analyzed invariant")
    }

    fn analyze_text_with_solver(source: &str) -> InvariantAnalysis {
        analyze_text_with_solver_limit(source, 100_000)
    }

    fn analyze_text_auto(source: &str) -> InvariantAnalysis {
        let report = analyze(
            &compile_text(source),
            Some("total"),
            &AnalysisOptions::default(),
        );
        report
            .invariants
            .into_iter()
            .next()
            .expect("analyzed invariant")
    }

    fn analyze_text_with_solver_limit(source: &str, max_evaluations: usize) -> InvariantAnalysis {
        let report = analyze_with_solver(
            &compile_text(source),
            Some("total"),
            &AnalysisOptions {
                max_evaluations,
                ..AnalysisOptions::default()
            },
            SolverMode::Z3,
        );
        report
            .invariants
            .into_iter()
            .next()
            .expect("analyzed invariant")
    }

    #[test]
    fn zero_input_assertions_evaluate_the_single_empty_assignment() {
        let program = compile_text(
            r"rule constant:
    O: result = O

rule never:
    X: absent = O

assert cardinality_pass:
    result

assert cardinality_fail:
    absent

assert implication_pass:
    O: result = O

assert implication_fail:
    O: result = X
",
        );
        let expected = [
            ("cardinality_pass", AnalysisVerdict::Passed),
            ("cardinality_fail", AnalysisVerdict::Failed),
            ("implication_pass", AnalysisVerdict::Passed),
            ("implication_fail", AnalysisVerdict::Failed),
        ];
        for (name, verdict) in expected {
            let report = analyze_with_solver(
                &program,
                Some(name),
                &AnalysisOptions::default(),
                SolverMode::Off,
            );
            let invariant = &report.invariants[0];
            assert_eq!(invariant.verdict, verdict, "{name}: {invariant:?}");
            assert_eq!(invariant.evaluated, 1, "{name}");
            assert_eq!(invariant.planned_evaluations, 1, "{name}");
            assert_eq!(
                invariant.completeness,
                Completeness::ThresholdPartitioned,
                "{name}"
            );
        }
    }

    /// Deliberately bypasses the production planner so compact exact strategies
    /// can be checked against a literal finite-domain oracle.
    fn raw_counterexamples(source: &str) -> Vec<Counterexample> {
        let program = compile_text(source);
        let invariant = program
            .ast()
            .declarations
            .iter()
            .find_map(|declaration| match declaration {
                Declaration::Invariant(invariant) if invariant.name.value == "total" => {
                    Some(invariant)
                }
                _ => None,
            })
            .expect("total invariant");
        let quantified = invariant
            .variables
            .iter()
            .map(|variable| {
                let entity = program
                    .entity(&variable.ty.value)
                    .expect("quantified entity");
                (variable, entity)
            })
            .collect::<Vec<_>>();
        let domains = concrete_domains(&program, &quantified, &BTreeSet::new(), true);
        let combinations = planned_evaluation_count(&domains).expect("finite test domain");

        (0..combinations)
            .filter_map(|ordinal| {
                find_invariant_violation(&program, invariant, &input_at(ordinal, &domains))
            })
            .collect()
    }

    fn input_int(counterexample: &Counterexample, field: &str) -> Option<i64> {
        counterexample
            .input
            .bindings
            .values()
            .next()?
            .fields
            .get(field)?
            .as_int()
    }

    fn binding_int(counterexample: &Counterexample, binding: &str, field: &str) -> Option<i64> {
        counterexample
            .input
            .bindings
            .get(binding)?
            .fields
            .get(field)?
            .as_int()
    }

    fn binding_decimal(
        counterexample: &Counterexample,
        binding: &str,
        field: &str,
    ) -> Option<Decimal> {
        counterexample
            .input
            .bindings
            .get(binding)?
            .fields
            .get(field)?
            .as_decimal()
    }

    fn int_field(optional: bool) -> FieldDecl {
        FieldDecl {
            name: Spanned::new("x".into(), Span::default()),
            ty: TypeRef::Int,
            ty_span: Span::default(),
            range: Some(RangeConstraint {
                start: NumericLiteral::Int(0),
                end: NumericLiteral::Int(3),
                start_inclusive: true,
                end_inclusive: true,
                span: Span::default(),
            }),
            domain: None,
            optional,
            span: Span::default(),
        }
    }

    #[test]
    fn boundary_values_include_endpoints() {
        let values = integer_values(&int_field(false), &BTreeSet::new(), false);
        assert!(values.contains(&Value::Int(0)));
        assert!(values.contains(&Value::Int(3)));
    }

    #[test]
    fn exhaustive_integer_values_cover_range() {
        let values = integer_values(&int_field(false), &BTreeSet::new(), true);
        assert_eq!(
            values,
            [Value::Int(0), Value::Int(1), Value::Int(2), Value::Int(3)]
        );
    }

    #[test]
    fn open_integer_endpoints_are_never_enumerated() {
        let mut field = int_field(false);
        let range = field.range.as_mut().expect("test range");
        range.start_inclusive = false;
        range.end_inclusive = false;
        let values = integer_values(&field, &BTreeSet::new(), true);
        assert_eq!(values, [Value::Int(1), Value::Int(2)]);
        assert_eq!(int_field_bounds(&field), Ok((1, 2)));
    }

    #[test]
    fn threshold_neighbors_are_generated() {
        let values = integer_values(
            &int_field(false),
            &BTreeSet::from([Decimal::from(2)]),
            false,
        );
        assert!(values.contains(&Value::Int(1)));
        assert!(values.contains(&Value::Int(2)));
        assert!(values.contains(&Value::Int(3)));
    }

    #[test]
    fn range_less_numbers_include_rule_boundaries() {
        let mut field = int_field(false);
        field.range = None;
        let values = integer_values(&field, &BTreeSet::from([Decimal::from(100)]), false);
        assert!(values.contains(&Value::Int(99)));
        assert!(values.contains(&Value::Int(100)));
        assert!(values.contains(&Value::Int(101)));
    }

    #[test]
    fn input_enumeration_is_stable() {
        let domains = vec![QuantifiedDomain {
            binding: "s".into(),
            entity: "Student".into(),
            fields: vec![FieldDomain {
                name: "x".into(),
                values: vec![Some(Value::Int(0)), Some(Value::Int(1))],
            }],
        }];
        let first = input_at(0, &domains);
        let second = input_at(1, &domains);
        assert_eq!(first.bindings["s"].fields["x"], Value::Int(0));
        assert_eq!(second.bindings["s"].fields["x"], Value::Int(1));
    }

    #[test]
    fn cartesian_enumeration_is_lexicographic_by_field_order() {
        let domains = vec![QuantifiedDomain {
            binding: "s".into(),
            entity: "E".into(),
            fields: vec![
                FieldDomain {
                    name: "a".into(),
                    values: vec![Some(Value::Int(0)), Some(Value::Int(1))],
                },
                FieldDomain {
                    name: "b".into(),
                    values: vec![Some(Value::Int(0)), Some(Value::Int(1))],
                },
            ],
        }];
        let second = input_at(1, &domains);
        let third = input_at(2, &domains);
        assert_eq!(second.bindings["s"].fields["a"], Value::Int(0));
        assert_eq!(second.bindings["s"].fields["b"], Value::Int(1));
        assert_eq!(third.bindings["s"].fields["a"], Value::Int(1));
        assert_eq!(third.bindings["s"].fields["b"], Value::Int(0));
    }

    #[test]
    fn planned_evaluation_overflow_is_not_saturated_into_an_exact_count() {
        let domains = vec![QuantifiedDomain {
            binding: "s".into(),
            entity: "E".into(),
            fields: (0..usize::BITS)
                .map(|index| FieldDomain {
                    name: format!("f{index}"),
                    values: vec![Some(Value::Bool(false)), Some(Value::Bool(true))],
                })
                .collect(),
        }];
        assert_eq!(planned_evaluation_count(&domains), None);
    }

    #[test]
    fn empty_or_inconclusive_report_is_not_successful() {
        assert!(!AnalysisReport::default().success());
        let report = AnalysisReport {
            invariants: vec![InvariantAnalysis {
                invariant: "c".into(),
                quantifier: InvariantQuantifier::All,
                verdict: AnalysisVerdict::Inconclusive,
                evaluated: 1,
                planned_evaluations: 2,
                completeness: Completeness::Truncated,
                solver: None,
                witness: None,
                counterexamples: Vec::new(),
                notes: Vec::new(),
            }],
            findings: Vec::new(),
        };
        assert!(!report.success());
    }

    #[test]
    fn human_report_summarizes_strategies_without_machine_labels_or_routine_notes() {
        let invariant =
            |name: &str, verdict, evaluated, planned_evaluations, completeness, solver, notes| {
                InvariantAnalysis {
                    invariant: name.into(),
                    quantifier: InvariantQuantifier::All,
                    verdict,
                    evaluated,
                    planned_evaluations,
                    completeness,
                    solver,
                    witness: None,
                    counterexamples: Vec::new(),
                    notes,
                }
            };
        let report = AnalysisReport {
            invariants: vec![
                invariant(
                    "exhaustive",
                    AnalysisVerdict::Passed,
                    40_804,
                    40_804,
                    Completeness::Exhaustive,
                    None,
                    Vec::new(),
                ),
                invariant(
                    "threshold",
                    AnalysisVerdict::Passed,
                    4,
                    4,
                    Completeness::ThresholdPartitioned,
                    None,
                    vec!["used an exact threshold partition: every representative stands for a region with identical relevant rule and assertion outcomes".into()],
                ),
                invariant(
                    "solver",
                    AnalysisVerdict::Passed,
                    0,
                    0,
                    Completeness::SolverExact,
                    Some(SolverMetadata {
                        backend: "z3".into(),
                        version: "Z3 4.15.2.0".into(),
                        logic: "QF_LIA".into(),
                    }),
                    vec!["the negated property is unsatisfiable in QF_LIA via Z3".into()],
                ),
                invariant(
                    "sampled",
                    AnalysisVerdict::Inconclusive,
                    12,
                    12,
                    Completeness::BoundarySampled,
                    None,
                    vec![
                        "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a counterexample is not a proof".into(),
                        "exact analysis is unavailable for this expression".into(),
                    ],
                ),
                invariant(
                    "truncated",
                    AnalysisVerdict::Inconclusive,
                    100,
                    2_000,
                    Completeness::Truncated,
                    None,
                    vec!["stopped at the configured evaluation limit of 100".into()],
                ),
            ],
            findings: Vec::new(),
        };

        let text = report.render_text();
        assert!(
            text.contains(
                "✓ exhaustive\n  proved for all inputs · all 40,804 combinations checked"
            )
        );
        assert!(text.contains("✓ threshold\n  proved for all inputs · 4 exact regions checked"));
        assert!(text.contains("✓ solver\n  proved for all inputs · exact solver (Z3)"));
        assert!(
            text.contains(
                "? sampled\n  inconclusive · 12 boundary samples checked · not exhaustive"
            )
        );
        assert!(text.contains("  reason · exact analysis is unavailable for this expression"));
        assert!(
            text.contains("? truncated\n  inconclusive · 100 of 2,000 evaluations · truncated")
        );
        for hidden in [
            "solver_exact",
            "threshold_partitioned",
            "negated property",
            "used an exact threshold partition",
            "stopped at the configured evaluation limit",
        ] {
            assert!(!text.contains(hidden), "unexpected `{hidden}` in:\n{text}");
        }
    }

    #[test]
    fn existential_cardinality_passes_when_one_exact_assignment_is_a_witness() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 4]
rule yes(e E):
    e.x = 2: d(e) = Yes
assert some total(e E):
    d(e)
",
            100,
        );

        assert_eq!(invariant.quantifier, InvariantQuantifier::Some);
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert!(invariant.evaluated < invariant.planned_evaluations);
        assert!(invariant.counterexamples.is_empty());
        let witness = invariant.witness.as_ref().expect("existential witness");
        assert_eq!(witness.bindings["e"].fields["x"], Value::Int(2));
        let json = serde_json::to_value(&invariant).unwrap();
        assert_eq!(json["quantifier"], "some");
        assert_eq!(json["witness"]["bindings"]["e"]["entity"], "E");
        let report = AnalysisReport {
            invariants: vec![invariant],
            findings: Vec::new(),
        };
        assert!(
            report
                .render_text()
                .contains("✓ total\n  satisfying input found · after 2 evaluations")
        );
        assert!(report.render_text().contains("  witness\n    e: E {"));
    }

    #[test]
    fn existential_exact_exhaustion_without_a_witness_is_conclusively_failed() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 4]
rule impossible(e E):
    e.x < 0: d(e) = Yes
assert some total(e E):
    d(e)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert!(matches!(
            invariant.completeness,
            Completeness::Exhaustive | Completeness::ThresholdPartitioned
        ));
        assert!(invariant.counterexamples.is_empty());
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("none satisfied the assertion"))
        );
        let report = AnalysisReport {
            invariants: vec![invariant],
            findings: Vec::new(),
        };
        assert!(
            report
                .render_text()
                .contains("✗ total\n  no satisfying input exists")
        );
    }

    #[test]
    fn existential_limited_search_without_a_witness_remains_inconclusive() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 4]
rule impossible(e E):
    e.x < 0: d(e) = Yes
assert some total(e E):
    d(e)
",
            0,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.evaluated, 0);
        assert!(invariant.planned_evaluations > 0);
        assert!(invariant.counterexamples.is_empty());
    }

    #[test]
    fn existential_search_crosses_multiple_bindings() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Yes
record Left:
    enabled: Bool
record Right:
    enabled: Bool
rule yes(left Left, right Right):
    left.enabled & right.enabled: d(left, right) = Yes
assert some total(left Left, right Right):
    d(left, right)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
        assert_eq!(invariant.evaluated, 4);
    }

    #[test]
    fn existential_implication_requires_a_true_premise_and_satisfied_expectation() {
        let source = r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 1]
rule yes(e E):
    e.x = 1: d(e) = Yes
assert some total(e E):
    e.x = 1: d(e) = Yes
";
        let invariant = analyze_text(source, 100);
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);

        let program = compile_text(source);
        let false_premise = Input {
            bindings: BTreeMap::from([(
                "e".into(),
                crate::engine::EntityInput {
                    entity: "E".into(),
                    fields: BTreeMap::from([("x".into(), Value::Int(0))]),
                },
            )]),
        };
        assert_eq!(
            replay_invariant_witness(&program, "total", &false_premise).unwrap_err(),
            "the existential property premise evaluates to X"
        );
    }

    #[test]
    fn existential_threshold_partition_proves_a_witness_in_a_huge_domain() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Exact
record E:
    x: Int [0, 1_000_000_000]
rule exact(e E):
    e.x = 50: d(e) = Exact
assert some total(e E):
    d(e)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.planned_evaluations, 3);
        assert_eq!(invariant.evaluated, 2);
        assert_eq!(
            invariant.witness.as_ref().unwrap().bindings["e"].fields["x"],
            Value::Int(50)
        );
    }

    #[test]
    fn existential_boundary_sample_witness_is_conclusive() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Exact
record E:
    x: Int [0, 1_000_000_000]
rule exact(e E):
    e.x + 1 = 50: d(e) = Exact
assert some total(e E):
    d(e)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert!(matches!(
            invariant.completeness,
            Completeness::BoundarySampled | Completeness::Truncated
        ));
        assert!(invariant.evaluated > 0);
        assert!(invariant.witness.is_some());
        assert!(invariant.counterexamples.is_empty());
    }

    #[test]
    fn existential_solver_results_are_replayed_as_witness_or_exact_refutation() {
        let witness = analyze_text_with_solver(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 1_000_000]
rule yes(e E):
    e.x = 37: d(e) = Yes
assert some total(e E):
    d(e)
",
        );
        assert_eq!(witness.verdict, AnalysisVerdict::Passed);
        assert_eq!(witness.completeness, Completeness::SolverExact);
        assert_eq!(witness.evaluated, 1);
        assert_eq!(
            witness.witness.as_ref().unwrap().bindings["e"].fields["x"],
            Value::Int(37)
        );

        let refuted = analyze_text_with_solver(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 1_000_000]
rule impossible(e E):
    e.x < 0: d(e) = Yes
assert some total(e E):
    d(e)
",
        );
        assert_eq!(refuted.verdict, AnalysisVerdict::Failed);
        assert_eq!(refuted.completeness, Completeness::SolverExact);
        assert!(refuted.witness.is_none());
        assert!(refuted.counterexamples.is_empty());
    }

    #[test]
    fn huge_int_range_is_proved_by_three_exact_regions() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    Exact
    High
record E:
    x: Int [0, 1_000_000_000]
rule low(s E):
    s.x < 50: d(s) = Low
rule exact(s E):
    s.x = 50: d(s) = Exact
rule high(s E):
    s.x > 50: d(s) = High
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 3);
        assert_eq!(invariant.planned_evaluations, 3);
        let report = AnalysisReport {
            invariants: vec![invariant],
            findings: Vec::new(),
        };
        assert!(
            report
                .render_text()
                .contains("proved for all inputs · 3 exact regions checked")
        );
    }

    #[test]
    fn exact_partition_finds_gap_at_threshold() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 1_000_000_000]
rule low(s E):
    s.x < 50: d(s) = Low
rule high(s E):
    s.x > 50: d(s) = High
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        assert_eq!(input_int(&invariant.counterexamples[0], "x"), Some(50));
    }

    #[test]
    fn exact_partition_finds_distinct_value_overlap_at_threshold() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 1_000_000_000]
rule low(s E):
    s.x <= 50: d(s) = Low
rule high(s E):
    s.x >= 50: d(s) = High
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );
        assert_eq!(input_int(&invariant.counterexamples[0], "x"), Some(50));
    }

    #[test]
    fn bool_and_enum_fields_are_crossed_exactly_while_unused_fields_are_collapsed() {
        let invariant = analyze_text(
            r"mod M
enum Mode:
    A
    B
enum Result:
    Yes
    No
record E:
    flag: Bool
    mode: Mode
    unused: String
rule yes_a(s E):
    s.flag & s.mode = A: d(s) = Yes
rule yes_b(s E):
    s.flag & s.mode = B: d(s) = Yes
rule no_a(s E):
    s.flag X & s.mode = A: d(s) = No
rule no_b(s E):
    s.flag X & s.mode = B: d(s) = No
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 4);
    }

    #[test]
    fn unsupported_rules_for_another_decision_do_not_disable_exact_partitioning() {
        let invariant = analyze_text(
            r#"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 1_000_000_000]
    text: String
rule low(s E):
    s.x < 50: d(s) = Low
rule high(s E):
    s.x >= 50: d(s) = High
rule string_rule(s E):
    s.text = "unsupported but irrelevant": unrelated(s) = O
assert total(s E):
    d(s)
"#,
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
    }

    #[test]
    fn direct_override_conditions_participate_in_the_exact_partition() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Base
    Special
record E:
    x: Int [0, 1_000_000_000]
rule base(s E):
    O: d(s) = Base
rule special(s E):
    s.x >= 50: d(s) = Special
rule prefer_special(s E):
    s.x >= 50: override base
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
    }

    #[test]
    fn optional_bool_override_keeps_missing_as_an_exact_unknown_region() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Base
    Special
record E:
    special: Bool?
    unused: String
rule base(s E):
    O: d(s) = Base
rule special(s E):
    s.special: d(s) = Special
rule prefer_special(s E):
    s.special: override base
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 3);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Unknown
        );
        assert!(
            !invariant.counterexamples[0].input.bindings["s"]
                .fields
                .contains_key("special")
        );
    }

    #[test]
    fn repeated_query_binding_supports_rule_parameter_permutation() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Yes
record E:
    value: Int [0, 1_000_000_000]
rule yes(left E, right E):
    left.value < 50 & right.value < 50: d(right, left) = Yes
assert total(s E):
    d(s, s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 2);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        assert_eq!(input_int(&invariant.counterexamples[0], "value"), Some(50));
    }

    #[test]
    fn shared_binding_resolver_matches_runtime_for_permuted_arguments() {
        let program = compile_text(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 2]
rule swapped(left E, right E):
    left.x = 2 & right.x = 1: d(right, left) = Yes
",
        );
        let query = Query::parse("d(a, b)").unwrap();
        let bindings = BTreeMap::from([("a".into(), "E".into()), ("b".into(), "E".into())]);
        let mapping = resolve_rule_bindings(
            program.rule("swapped").unwrap(),
            program.decision("d").unwrap(),
            &query,
            &bindings,
        )
        .unwrap();
        assert_eq!(mapping["left"], "b");
        assert_eq!(mapping["right"], "a");

        let mut input = Input::new();
        input.insert("a", "E", BTreeMap::from([("x".into(), Value::Int(1))]));
        input.insert("b", "E", BTreeMap::from([("x".into(), Value::Int(2))]));
        let evaluation = evaluate_query(&program, &input, &query).unwrap();
        assert!(matches!(
            evaluation.result.status,
            DecisionStatus::Resolved { ref values } if values.len() == 1
        ));
    }

    #[test]
    fn two_independent_bindings_of_the_same_entity_are_partitioned_separately() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    LL
    LH
    HL
    HH
record E:
    x: Int [0, 1_000_000_000]
rule ll(left E, right E):
    left.x < 50 & right.x < 100: d(left, right) = LL
rule lh(left E, right E):
    left.x < 50 & right.x >= 100: d(left, right) = LH
rule hl(left E, right E):
    left.x >= 50 & right.x < 100: d(left, right) = HL
rule hh(left E, right E):
    left.x >= 50 & right.x >= 100: d(left, right) = HH
assert total(a E, b E):
    d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn multi_binding_gap_witness_preserves_each_independent_input() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    LL
    LH
    HL
record E:
    x: Int [0, 1_000_000_000]
rule ll(left E, right E):
    left.x < 50 & right.x < 100: d(left, right) = LL
rule lh(left E, right E):
    left.x < 50 & right.x >= 100: d(left, right) = LH
rule hl(left E, right E):
    left.x >= 50 & right.x < 100: d(left, right) = HL
assert total(a E, b E):
    d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "a", "x"),
            Some(50)
        );
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "b", "x"),
            Some(100)
        );
    }

    #[test]
    fn independent_query_argument_permutation_assigns_cuts_to_the_actual_bindings() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Yes
record E:
    x: Int [0, 1_000_000_000]
rule yes(left E, right E):
    left.x < 100 & right.x < 50: d(right, left) = Yes
assert total(a E, b E):
    d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "a", "x"),
            Some(0)
        );
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "b", "x"),
            Some(100)
        );
    }

    #[test]
    fn different_quantified_entity_types_get_independent_exact_domains() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 1_000_000_000]
record Member:
    premium: Bool
rule premium(order Order, member Member):
    member.premium: d(order, member) = Free
rule large(order Order, member Member):
    member.premium X & order.amount >= 50: d(order, member) = Free
rule small(order Order, member Member):
    member.premium X & order.amount < 50: d(order, member) = Paid
assert total(o Order, m Member):
    d(o, m)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn premise_only_quantified_binding_contributes_its_exact_bool_and_int_regions() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Free
record Order:
    amount: Int [0, 1_000_000_000]
record Customer:
    vip: Bool
    score: Int [0, 1_000_000_000]
rule free(order Order):
    O: d(order) = Free
assert total(o Order, c Customer):
    c.vip & c.score >= 100: d(o) = Free
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn multi_binding_cross_field_predicate_falls_back_instead_of_claiming_proof() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Less
    NotLess
record E:
    x: Int [0, 1_000_000_000]
rule less(left E, right E):
    left.x < right.x: d(left, right) = Less
rule not_less(left E, right E):
    left.x >= right.x: d(left, right) = NotLess
assert total(a E, b E):
    d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("compares two input fields"))
        );
    }

    #[test]
    fn solver_finds_a_relational_gap_and_replays_the_model() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 100_000]
record Coupon:
    discount: Int [0, 100_000]
rule free(order Order, coupon Coupon):
    order.amount - coupon.discount > 50_000: d(order, coupon) = Free
rule paid(order Order, coupon Coupon):
    order.amount - coupon.discount < 50_000: d(order, coupon) = Paid
assert total(order Order, coupon Coupon):
    d(order, coupon)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        let amount = binding_int(&invariant.counterexamples[0], "order", "amount").unwrap();
        let discount = binding_int(&invariant.counterexamples[0], "coupon", "discount").unwrap();
        assert_eq!(amount - discount, 50_000);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_LIA");
    }

    #[test]
    fn solver_proves_relational_totality_without_enumerating_the_raw_product() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 100_000]
record Coupon:
    discount: Int [0, 100_000]
rule free(order Order, coupon Coupon):
    order.amount - coupon.discount >= 50_000: d(order, coupon) = Free
rule paid(order Order, coupon Coupon):
    order.amount - coupon.discount < 50_000: d(order, coupon) = Paid
assert total(order Order, coupon Coupon):
    d(order, coupon)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn solver_distinguishes_different_value_overlap_from_same_value_merge() {
        let conflicting = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record A:
    x: Int [0, 100_000]
record B:
    y: Int [0, 100_000]
rule free(a A, b B):
    a.x - b.y >= 50_000: d(a, b) = Free
rule paid(a A, b B):
    a.x - b.y <= 50_000: d(a, b) = Paid
assert total(a A, b B):
    d(a, b)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );

        let merged = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
record A:
    x: Int [0, 100_000]
record B:
    y: Int [0, 100_000]
rule upper(a A, b B):
    a.x - b.y >= 50_000: d(a, b) = Free
rule lower(a A, b B):
    a.x - b.y <= 50_000: d(a, b) = Free
assert total(a A, b B):
    d(a, b)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_handles_implication_bool_enum_and_constant_scaled_linear_terms() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
enum Tier:
    Standard
    Preferred
record Order:
    amount: Int [0, 100_000]
record Customer:
    credit: Int [0, 100_000]
    premium: Bool
    tier: Tier
rule preferred(order Order, customer Customer):
    customer.premium & customer.tier = Preferred: d(order, customer) = Free
rule amount(order Order, customer Customer):
    customer.premium X & 2 * order.amount - customer.credit >= 50_000: d(order, customer) = Free
rule paid(order Order, customer Customer):
    customer.premium X & 2 * order.amount - customer.credit < 50_000: d(order, customer) = Paid
rule standard_premium(order Order, customer Customer):
    customer.premium & customer.tier = Standard: d(order, customer) = Paid
assert total(order Order, customer Customer):
    customer.premium & customer.tier = Preferred: d(order, customer) = Free
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_proves_direct_decimal_field_relations_without_sampling() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    WithinLimit
    Review
record Expense:
    claimed: Decimal [0.00, 1_000_000.00]
    approved: Decimal [0.00, 1_000_000.00]
fn claimed_amount(e Expense) Decimal:
    e.claimed
rule within(e Expense):
    claimed_amount(e) <= e.approved: audit(e) = WithinLimit
rule review(e Expense):
    claimed_amount(e) > e.approved: audit(e) = Review
assert total(e Expense):
    audit(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_LIA");
    }

    #[test]
    fn solver_replays_a_decimal_gap_at_equal_field_values() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    Lower
    Higher
record Quote:
    offered: Decimal [0.00, 1_000_000.00]
    limit: Decimal [0.00, 1_000_000.00]
rule lower(q Quote):
    q.offered < q.limit: classify(q) = Lower
rule higher(q Quote):
    q.offered > q.limit: classify(q) = Higher
assert total(q Quote):
    classify(q)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 1);
        let offered = binding_decimal(&invariant.counterexamples[0], "q", "offered").unwrap();
        let limit = binding_decimal(&invariant.counterexamples[0], "q", "limit").unwrap();
        assert_eq!(offered, limit);
    }

    #[test]
    fn solver_handles_mixed_int_decimal_comparisons_and_scale_28_neighbors() {
        let mixed = analyze_text_auto(
            r"mod M
enum Result:
    Below
    AtOrAbove
record E:
    amount: Decimal [0.0, 100.0]
    limit: Int [0, 100]
rule below(e E):
    e.amount < e.limit: d(e) = Below
rule at_or_above(e E):
    e.amount >= e.limit: d(e) = AtOrAbove
assert total(e E):
    d(e)
",
        );
        assert_eq!(mixed.verdict, AnalysisVerdict::Passed);
        assert_eq!(mixed.completeness, Completeness::SolverExact);

        let adjacent = analyze_text_auto(
            r"mod M
enum Result:
    Zero
    Quantum
record E:
    amount: Decimal [0.0, 0.0000000000000000000000000001]
rule at_zero(e E):
    e.amount = 0: d(e) = Zero
rule at_quantum(e E):
    e.amount = 0.0000000000000000000000000001: d(e) = Quantum
assert total(e E):
    d(e)
",
        );
        assert_eq!(adjacent.verdict, AnalysisVerdict::Passed);
        assert_eq!(adjacent.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_materializes_a_96_bit_decimal_mantissa() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    Below
record E:
    amount: Decimal [7922816251426433759354395033.4, 7922816251426433759354395033.5]
rule below(e E):
    e.amount < 7922816251426433759354395033.5: d(e) = Below
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(
            binding_decimal(&invariant.counterexamples[0], "e", "amount").unwrap(),
            parse_decimal("7922816251426433759354395033.5").unwrap()
        );
    }

    #[test]
    fn solver_inlines_overflow_safe_entity_derives() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 100_000]
record Coupon:
    discount: Int [0, 100_000]
fn net(order Order, coupon Coupon) Int:
    order.amount - coupon.discount
rule free(order Order, coupon Coupon):
    net(order, coupon) >= 50_000: d(order, coupon) = Free
rule paid(order Order, coupon Coupon):
    net(order, coupon) < 50_000: d(order, coupon) = Paid
assert total(order Order, coupon Coupon):
    d(order, coupon)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_proves_exact_input_dependent_decimal_arithmetic() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Any
record E:
    left: Decimal [0.0, 1.0]
    right: Decimal [0.0, 1.0]
    unit: Decimal [1.0, 1.0]
fn scaled(value Decimal, factor Decimal) Decimal:
    value * factor
fn combined(e E) Decimal:
    scaled(e.left + e.right, e.unit)
rule any(e E):
    combined(e) >= 0: d(e) = Any
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_NIA");
    }

    #[test]
    fn solver_replays_inexact_decimal_add_multiply_and_divide() {
        for expression in [
            "e.maximum_tenth + 0.1",
            "e.quantum * 0.1",
            "e.unit / 3",
            "e.unit / e.nothing",
        ] {
            let source = format!(
                r"mod M
enum Result:
    Any
record E:
    maximum_tenth: Decimal [7922816251426433759354395033.5, 7922816251426433759354395033.5]
    quantum: Decimal [0.0000000000000000000000000001, 0.0000000000000000000000000001]
    unit: Decimal [1.0, 1.0]
    nothing: Decimal [0.0, 0.0]
rule any(e E):
    {expression} >= 0: d(e) = Any
assert total(e E):
    d(e)
"
            );
            let invariant = analyze_text_with_solver(&source);
            assert_eq!(
                invariant.verdict,
                AnalysisVerdict::Failed,
                "{expression}: {:?}",
                invariant.notes
            );
            assert_eq!(invariant.completeness, Completeness::SolverExact);
            assert_eq!(
                invariant.counterexamples[0].kind,
                CounterexampleKind::Conflict
            );
        }
    }

    #[test]
    fn solver_matches_boolean_conflict_absorption_and_premise_conflict() {
        let short_circuit = analyze_text_with_solver(
            r"mod M
enum Result:
    Any
record E:
    x: Decimal [1.0, 1.0]
rule skipped_left_false(e E):
    X & e.x / 0 > 0: d(e) = Any
rule skipped_right_false(e E):
    e.x / 0 > 0 & X: d(e) = Any
rule applied_left_true(e E):
    O | e.x / 0 > 0: d(e) = Any
rule applied_right_true(e E):
    e.x / 0 > 0 | O: d(e) = Any
assert total(e E):
    d(e)
",
        );
        assert_eq!(short_circuit.verdict, AnalysisVerdict::Passed);
        assert_eq!(short_circuit.completeness, Completeness::SolverExact);

        let premise = analyze_text_with_solver(
            r"mod M
enum Result:
    Any
record E:
    x: Decimal [1.0, 1.0]
rule any(e E):
    O: d(e) = Any
assert total(e E):
    e.x / 0 > 0: d(e) = Any
",
        );
        assert_eq!(premise.verdict, AnalysisVerdict::Failed);
        assert_eq!(premise.completeness, Completeness::SolverExact);
        assert_eq!(
            premise.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
    }

    #[test]
    fn solver_handles_dynamic_decimal_candidates_and_same_value_merge() {
        let merged = analyze_text_with_solver(
            r"mod M
record E:
    amount: Decimal [0.0, 1.0]
rule first(e E):
    e.amount >= 0: d(e) = e.amount + 0
rule second(e E):
    e.amount <= 1: d(e) = e.amount
assert total(e E):
    d(e)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);

        let conflicting = analyze_text_with_solver(
            r"mod M
record E:
    amount: Decimal [0.0, 1.0]
rule first(e E):
    e.amount >= 0: d(e) = e.amount
rule second(e E):
    e.amount <= 1: d(e) = e.amount + 1
assert total(e E):
    d(e)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );

        let expected = analyze_text_with_solver(
            r"mod M
record E:
    amount: Decimal [0.0, 1.0]
rule copy(e E):
    O: d(e) = e.amount + 0
assert total(e E):
    e.amount = 0: d(e) = 0
",
        );
        assert_eq!(expected.verdict, AnalysisVerdict::Passed);
        assert_eq!(expected.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_handles_dynamic_bool_candidates_and_same_value_merge() {
        let merged = analyze_text_with_solver(
            r"mod M
record E:
    value: Bool
    guard: Bool
rule first(e E):
    e.guard | e.guard X: d(e) = e.value
rule second(e E):
    e.guard X | e.guard: d(e) = e.value X X
assert total(e E):
    d(e)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);

        let conflicting = analyze_text_with_solver(
            r"mod M
record E:
    value: Bool
    guard: Bool
rule first(e E):
    e.guard | e.guard X: d(e) = e.value
rule second(e E):
    e.guard X | e.guard: d(e) = e.value X
assert total(e E):
    d(e)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );
    }

    #[test]
    fn solver_handles_dynamic_int_candidates_and_same_value_merge() {
        let merged = analyze_text_with_solver(
            r"mod M
record E:
    x: Int [0, 10]
rule first(e E):
    e.x >= 0: d(e) = e.x + 0
rule second(e E):
    e.x <= 10: d(e) = e.x
assert total(e E):
    d(e)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);

        let conflicting = analyze_text_with_solver(
            r"mod M
record E:
    x: Int [0, 10]
rule first(e E):
    e.x >= 0: d(e) = e.x
rule second(e E):
    e.x <= 10: d(e) = e.x + 1
assert total(e E):
    d(e)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );
    }

    #[test]
    fn solver_tracks_dynamic_int_candidate_overflow_only_while_active() {
        let overflowing = analyze_text_with_solver_limit(
            r"mod M
record E:
    x: Int [9_223_372_036_854_775_806, 9_223_372_036_854_775_807]
rule increment(e E):
    O: d(e) = e.x + 1
assert total(e E):
    d(e)
",
            1,
        );
        assert_eq!(overflowing.verdict, AnalysisVerdict::Failed);
        assert_eq!(overflowing.completeness, Completeness::SolverExact);
        assert_eq!(
            overflowing.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
        let x = binding_int(&overflowing.counterexamples[0], "e", "x").unwrap();
        assert!(x.checked_add(1).is_none());

        let inactive_at_maximum = analyze_text_with_solver(
            r"mod M
record E:
    x: Int [9_223_372_036_854_775_806, 9_223_372_036_854_775_807]
rule increment(e E):
    e.x < 9_223_372_036_854_775_807: d(e) = e.x + 1
rule maximum(e E):
    e.x = 9_223_372_036_854_775_807: d(e) = e.x
assert total(e E):
    d(e)
",
        );
        assert_eq!(inactive_at_maximum.verdict, AnalysisVerdict::Passed);
        assert_eq!(inactive_at_maximum.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_exact_many_cardinality_accepts_values_but_rejects_runtime_conflict() {
        let valid = analyze_text_with_solver(
            r"mod M
record E:
    x: Int [0, 10]
rule first(e E):
    e.x >= 0: d(e) = e.x
rule second(e E):
    e.x <= 10: d(e) = e.x + 1
assert total(e E):
    d(e)*
",
        );
        assert_eq!(valid.verdict, AnalysisVerdict::Passed);
        assert_eq!(valid.completeness, Completeness::SolverExact);

        let conflicted = analyze_text_with_solver_limit(
            r"mod M
record E:
    x: Int [9_223_372_036_854_775_807, 9_223_372_036_854_775_807]
rule overflow(e E):
    O: d(e) = e.x + 1
assert total(e E):
    d(e)*
",
            1,
        );
        assert_eq!(conflicted.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicted.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicted.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
    }

    #[test]
    fn solver_materializes_forced_bool_and_enum_sat_witnesses() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Mode:
    A
    B
enum Result:
    Covered
record E:
    enabled: Bool
    mode: Mode
rule mode_a(e E):
    e.mode = A: d(e) = Covered
rule disabled_b(e E):
    e.enabled X & e.mode = B: d(e) = Covered
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        let fields = &invariant.counterexamples[0].input.bindings["e"].fields;
        assert_eq!(fields["enabled"], Value::Bool(true));
        assert_eq!(
            fields["mode"],
            Value::Enum {
                type_name: "Mode".into(),
                variant: "B".into(),
            }
        );
    }

    #[test]
    fn solver_proves_nested_int_min_max_totality_and_finds_its_boundary_gap() {
        let total = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 100_000]
record Coupon:
    discount: Int [0, 100_000]
fn payable(order Order, coupon Coupon) Int:
    max(0, order.amount - coupon.discount)
fn capped(order Order, coupon Coupon) Int:
    min(50_000, payable(order, coupon))
rule free(order Order, coupon Coupon):
    capped(order, coupon) >= 50_000: d(order, coupon) = Free
rule paid(order Order, coupon Coupon):
    capped(order, coupon) < 50_000: d(order, coupon) = Paid
assert total(order Order, coupon Coupon):
    d(order, coupon)
",
        );
        assert_eq!(total.verdict, AnalysisVerdict::Passed);
        assert_eq!(total.completeness, Completeness::SolverExact);

        let gap = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 100_000]
record Coupon:
    discount: Int [0, 100_000]
fn payable(order Order, coupon Coupon) Int:
    max(0, order.amount - coupon.discount)
fn capped(order Order, coupon Coupon) Int:
    min(50_000, payable(order, coupon))
rule free(order Order, coupon Coupon):
    capped(order, coupon) > 50_000: d(order, coupon) = Free
rule paid(order Order, coupon Coupon):
    capped(order, coupon) < 50_000: d(order, coupon) = Paid
assert total(order Order, coupon Coupon):
    d(order, coupon)
",
        );
        assert_eq!(gap.verdict, AnalysisVerdict::Failed);
        assert_eq!(gap.completeness, Completeness::SolverExact);
        let amount = binding_int(&gap.counterexamples[0], "order", "amount").unwrap();
        let discount = binding_int(&gap.counterexamples[0], "coupon", "discount").unwrap();
        assert_eq!((amount - discount).clamp(0, 50_000), 50_000);
    }

    #[test]
    fn solver_proves_int_abs_totality_and_finds_its_boundary_gap() {
        let total = analyze_text_with_solver(
            r"mod M
enum Result:
    Near
    Far
record Point:
    x: Int [0, 100_000]
fn distance(left Point, right Point) Int:
    abs(left.x - right.x)
rule far(left Point, right Point):
    distance(left, right) >= 50_000: d(left, right) = Far
rule near(left Point, right Point):
    distance(left, right) < 50_000: d(left, right) = Near
assert total(left Point, right Point):
    d(left, right)
",
        );
        assert_eq!(total.verdict, AnalysisVerdict::Passed);
        assert_eq!(total.completeness, Completeness::SolverExact);

        let gap = analyze_text_with_solver(
            r"mod M
enum Result:
    Near
    Far
record Point:
    x: Int [0, 100_000]
fn distance(left Point, right Point) Int:
    abs(left.x - right.x)
rule far(left Point, right Point):
    distance(left, right) > 50_000: d(left, right) = Far
rule near(left Point, right Point):
    distance(left, right) < 50_000: d(left, right) = Near
assert total(left Point, right Point):
    d(left, right)
",
        );
        assert_eq!(gap.verdict, AnalysisVerdict::Failed);
        assert_eq!(gap.completeness, Completeness::SolverExact);
        let left = binding_int(&gap.counterexamples[0], "left", "x").unwrap();
        let right = binding_int(&gap.counterexamples[0], "right", "x").unwrap();
        assert_eq!(left.abs_diff(right), 50_000);
    }

    #[test]
    fn solver_replays_overflowing_min_max_arguments_even_when_they_are_not_selected() {
        for builtin in ["max", "min"] {
            for expression in [
                format!("{builtin}(e.x + 1, 0)"),
                format!("{builtin}(0, e.x + 1)"),
            ] {
                let source = format!(
                    r"mod M
enum Result:
    Any
record E:
    x: Int [0, 9_223_372_036_854_775_807]
fn selected(e E) Int:
    {expression}
rule any(e E):
    selected(e) >= 0: d(e) = Any
assert total(e E):
    d(e)
"
                );
                let invariant = analyze_text_with_solver_limit(&source, 1);
                assert_eq!(invariant.completeness, Completeness::SolverExact);
                assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
                assert_eq!(
                    binding_int(&invariant.counterexamples[0], "e", "x"),
                    Some(i64::MAX),
                    "{expression}"
                );
            }
        }
    }

    #[test]
    fn solver_replays_abs_overflow_at_i64_min() {
        let invariant = analyze_text_with_solver_limit(
            r"mod M
enum Result:
    Any
record E:
    x: Int [-9_223_372_036_854_775_808, 9_223_372_036_854_775_807]
fn magnitude(e E) Int:
    abs(e.x)
rule any(e E):
    magnitude(e) >= 0: d(e) = Any
assert total(e E):
    d(e)
",
            1,
        );
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "e", "x"),
            Some(i64::MIN)
        );
    }

    #[test]
    fn solver_models_direct_override_activity_exactly() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Free
    Paid
record A:
    x: Int [0, 100_000]
record B:
    y: Int [0, 100_000]
rule base(a A, b B):
    O: d(a, b) = Paid
rule special(a A, b B):
    a.x >= b.y: d(a, b) = Free
rule prefer_special(a A, b B):
    a.x >= b.y: override base
assert total(a A, b B):
    d(a, b)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_and_exhaustive_modes_agree_on_a_small_relational_gap() {
        let source = r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 2]
rule low(a E, b E):
    a.x + b.x < 0: d(a, b) = Low
rule high(a E, b E):
    a.x + b.x > 0: d(a, b) = High
assert total(a E, b E):
    d(a, b)
";
        let exhaustive = analyze_text(source, 100);
        let automatic = analyze_text_auto(source);
        let solved = analyze_text_with_solver_limit(source, 1);
        assert_eq!(exhaustive.verdict, AnalysisVerdict::Failed);
        assert_eq!(exhaustive.completeness, Completeness::Exhaustive);
        assert_eq!(automatic.verdict, exhaustive.verdict);
        assert_eq!(automatic.completeness, Completeness::SolverExact);
        assert_eq!(automatic.evaluated, 1);
        assert_eq!(automatic.solver.as_ref().unwrap().logic, "QF_LIA");
        assert_eq!(solved.verdict, exhaustive.verdict);
        assert_eq!(solved.completeness, Completeness::SolverExact);
        let sum = binding_int(&solved.counterexamples[0], "a", "x").unwrap()
            + binding_int(&solved.counterexamples[0], "b", "x").unwrap();
        assert_eq!(sum, 0);
    }

    #[test]
    fn embedded_solver_counterexample_is_deterministic_across_repeated_runs() {
        let source = r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 10]
rule lower(left E, right E):
    left.x < right.x: d(left, right) = Low
rule higher(left E, right E):
    left.x > right.x: d(left, right) = High
assert total(left E, right E):
    d(left, right)
";
        let first = analyze_text_with_solver(source);
        assert_eq!(first.verdict, AnalysisVerdict::Failed);
        assert_eq!(first.completeness, Completeness::SolverExact);
        let expected = serde_json::to_value(&first).unwrap();
        for _ in 0..5 {
            assert_eq!(
                serde_json::to_value(analyze_text_with_solver(source)).unwrap(),
                expected
            );
        }
    }

    #[test]
    fn embedded_solver_counterexample_is_stable_under_rule_declaration_order() {
        let first_source = r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 10]
rule lower(left E, right E):
    left.x < right.x: d(left, right) = Low
rule higher(left E, right E):
    left.x > right.x: d(left, right) = High
assert total(left E, right E):
    d(left, right)
";
        let second_source = first_source.replace(
            "rule lower(left E, right E):\n    left.x < right.x: d(left, right) = Low\nrule higher(left E, right E):\n    left.x > right.x: d(left, right) = High",
            "rule higher(left E, right E):\n    left.x > right.x: d(left, right) = High\nrule lower(left E, right E):\n    left.x < right.x: d(left, right) = Low",
        );
        let first = analyze_text_with_solver(first_source);
        let second = analyze_text_with_solver(&second_source);
        assert_eq!(first.verdict, second.verdict);
        assert_eq!(first.completeness, second.completeness);
        assert_eq!(first.solver, second.solver);
        assert_eq!(
            first.counterexamples[0].kind,
            second.counterexamples[0].kind
        );
        assert_eq!(
            first.counterexamples[0].input,
            second.counterexamples[0].input
        );
    }

    #[test]
    fn solver_outcome_boundary_rejects_unknown_and_incomplete_replay() {
        let program = compile_text(
            r"mod M
record E:
    maybe: Bool?
rule present(e E):
    e.maybe: d(e) = O
assert total(e E):
    d(e)
",
        );
        let invariant = program.invariant("total").unwrap();
        assert_eq!(
            solver_outcome_analysis(
                &program,
                invariant,
                SolverOutcome::Unknown("timeout".into())
            )
            .unwrap_err(),
            "embedded solver was inconclusive: timeout"
        );
        assert_eq!(
            solver_outcome_analysis(
                &program,
                invariant,
                SolverOutcome::Unavailable("disabled".into())
            )
            .unwrap_err(),
            "embedded solver unavailable: disabled"
        );

        let mut input = Input::new();
        input.insert("e", "E", BTreeMap::new());
        let replay_error = solver_outcome_analysis(
            &program,
            invariant,
            SolverOutcome::Counterexample {
                input,
                metadata: SolverMetadata {
                    backend: "test".into(),
                    version: "test".into(),
                    logic: "QF_LIA".into(),
                },
            },
        )
        .unwrap_err();
        assert!(replay_error.contains("replay needed additional input"));
        assert!(replay_error.contains("e.maybe"));
    }

    #[test]
    fn planner_prefers_a_tiny_threshold_quotient_to_small_raw_enumeration() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 100]
rule low(e E):
    e.x < 50: d(e) = Low
rule high(e E):
    e.x >= 50: d(e) = High
assert total(e E):
    d(e)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
        assert_eq!(invariant.planned_evaluations, 2);
    }

    #[test]
    fn planner_honors_explicit_z3_before_a_compact_threshold_quotient() {
        let invariant = analyze_text_with_solver(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 100]
rule low(e E):
    e.x < 50: d(e) = Low
rule high(e E):
    e.x >= 50: d(e) = High
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn planner_uses_solver_before_a_large_supported_cartesian_product() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    Any
record E:
    b0: Bool
    b1: Bool
    b2: Bool
    b3: Bool
    b4: Bool
    b5: Bool
    b6: Bool
    b7: Bool
    b8: Bool
    b9: Bool
    b10: Bool
rule any(e E):
    (e.b0 | e.b0 X) & (e.b1 | e.b1 X) & (e.b2 | e.b2 X) & (e.b3 | e.b3 X) & (e.b4 | e.b4 X) & (e.b5 | e.b5 X) & (e.b6 | e.b6 X) & (e.b7 | e.b7 X) & (e.b8 | e.b8 X) & (e.b9 | e.b9 X) & (e.b10 | e.b10 X): d(e) = Any
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn planner_uses_bounded_qf_nia_before_a_finite_exact_product() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    Any
record E:
    x: Int [0, 32]
    y: Int [0, 32]
rule any(e E):
    e.x * e.y >= 0: d(e) = Any
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_NIA");
    }

    #[test]
    fn planner_solves_exact_decimal_division_before_small_exhaustive() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    Any
record E:
    x: Int [0, 2]
rule any(e E):
    e.x / 1 >= 0: d(e) = Any
assert total(e E):
    d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_LIA");
    }

    #[test]
    fn finite_string_and_decimal_domains_are_exhaustive() {
        let invariant = analyze_text_auto(
            r#"mod M
enum Result:
    Draft
    Approved
record E:
    status: String {"draft", "approved"}
    rate: Decimal {0.05, 0.10}
rule draft(e E):
    e.status = "draft" & e.rate >= 0.05: d(e) = Draft
rule approved(e E):
    e.status = "approved" & e.rate >= 0.05: d(e) = Approved
assert total(e E):
    d(e)
"#,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::Exhaustive);
        assert_eq!(invariant.evaluated, 4);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn solver_replays_symbolic_multiplication_overflow() {
        let invariant = analyze_text_with_solver_limit(
            r"mod M
enum Result:
    Any
record E:
    x: Int [0, 9_223_372_036_854_775_807]
rule any(e E):
    e.x * e.x >= 0: d(e) = Any
assert total(e E):
    d(e)
",
            1,
        );
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_NIA");
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
        let x = binding_int(&invariant.counterexamples[0], "e", "x").unwrap();
        assert!(x.checked_mul(x).is_none());
    }

    #[test]
    fn planner_solves_shipping_style_max_derive_without_40_804_evaluations() {
        let invariant = analyze_text_auto(
            r"mod M
enum Result:
    Free
    Paid
record Order:
    amount: Int [0, 100]
    discount: Int [0, 100]
    remote: Bool
    approved: Bool
fn payable(o Order) Int:
    max(0, o.amount - o.discount)
rule normal_free(o Order):
    payable(o) >= 50 & o.remote X: shipping(o) = Free
rule normal_paid(o Order):
    payable(o) < 50 & o.remote X: shipping(o) = Paid
rule remote_paid(o Order):
    o.remote: shipping(o) = Paid
rule approved_remote(o Order):
    o.remote & o.approved & payable(o) >= 50:
        shipping(o) = Free
        override remote_paid
assert total(o Order):
    shipping(o)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn solver_replays_potential_intermediate_i64_overflow() {
        let invariant = analyze_text_with_solver_limit(
            r"mod M
enum Result:
    Less
    NotLess
record E:
    x: Int
rule less(a E, b E):
    a.x - b.x < 0: d(a, b) = Less
rule not_less(a E, b E):
    a.x - b.x >= 0: d(a, b) = NotLess
assert total(a E, b E):
    d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
        let left = binding_int(&invariant.counterexamples[0], "a", "x").unwrap();
        let right = binding_int(&invariant.counterexamples[0], "b", "x").unwrap();
        assert!(left.checked_sub(right).is_none());
    }

    #[test]
    fn override_rule_with_ambiguous_same_type_extra_binding_falls_back() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Base
    Target
record Query:
    enabled: Bool
record Context:
    x: Int [0, 1_000_000_000]
rule target(query Query, context Context):
    context.x < 50: d(query) = Target
rule suppress_target(query Query, context Context):
    context.x >= 50: override target
rule base(query Query):
    O: d(query) = Base
assert total(q Query, a Context, b Context):
    d(q)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("ambiguous quantified binding"))
        );
    }

    #[test]
    fn shared_binding_ambiguity_matches_runtime_rule_skipping() {
        let program = compile_text(
            r"mod M
enum Result:
    Base
    Target
record Query:
    enabled: Bool
record Context:
    x: Int [0, 100]
rule target(query Query, context Context):
    context.x < 50: d(query) = Target
rule suppress_target(query Query, context Context):
    context.x >= 50: override target
rule base(query Query):
    O: d(query) = Base
",
        );
        let query = Query::parse("d(q)").unwrap();
        let bindings = BTreeMap::from([
            ("q".into(), "Query".into()),
            ("a".into(), "Context".into()),
            ("b".into(), "Context".into()),
        ]);
        for rule in ["target", "suppress_target"] {
            let error = resolve_rule_bindings(
                program.rule(rule).unwrap(),
                program.decision("d").unwrap(),
                &query,
                &bindings,
            )
            .unwrap_err();
            assert!(error.contains("ambiguous quantified binding"));
        }

        let mut input = Input::new();
        input.insert(
            "q",
            "Query",
            BTreeMap::from([("enabled".into(), Value::Bool(false))]),
        );
        input.insert(
            "a",
            "Context",
            BTreeMap::from([("x".into(), Value::Int(0))]),
        );
        input.insert(
            "b",
            "Context",
            BTreeMap::from([("x".into(), Value::Int(100))]),
        );
        let evaluation = evaluate_query(&program, &input, &query).unwrap();
        assert!(matches!(
            evaluation.result.status,
            DecisionStatus::Resolved { ref values }
                if values.iter().any(|value| value.to_string() == "Result.Base")
        ));
    }

    #[test]
    fn two_binding_partition_matches_exhaustive_counterexample_on_small_ranges() {
        let source = r"mod M
enum Result:
    Present
record E:
    x: Int [0, 2]
rule present(left E, right E):
    left.x != 1 | right.x != 2: d(left, right) = Present
assert total(a E, b E):
    d(a, b)
";
        let exhaustive = raw_counterexamples(source);
        let partitioned = analyze_text(source, 8);
        assert_eq!(partitioned.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(partitioned.verdict, AnalysisVerdict::Failed);
        assert_eq!(exhaustive[0].input, partitioned.counterexamples[0].input);
        assert_eq!(
            binding_int(&partitioned.counterexamples[0], "a", "x"),
            Some(1)
        );
        assert_eq!(
            binding_int(&partitioned.counterexamples[0], "b", "x"),
            Some(2)
        );
    }

    #[test]
    fn implication_premise_thresholds_are_part_of_the_exact_partition() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 1_000_000_000]
rule low(s E):
    s.x < 50: d(s) = Low
rule high(s E):
    s.x >= 50: d(s) = High
assert total(s E):
    s.x >= 50: d(s) = High
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
    }

    #[test]
    fn optional_int_missing_is_an_exact_singleton_region() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Negative
    Nonnegative
record E:
    x: Int?
rule negative(s E):
    s.x < 0: d(s) = Negative
rule nonnegative(s E):
    s.x >= 0: d(s) = Nonnegative
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 3);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Unknown
        );
        assert!(
            !invariant.counterexamples[0].input.bindings["s"]
                .fields
                .contains_key("x")
        );
    }

    #[test]
    fn fractional_thresholds_partition_the_integer_domain_with_floor_and_ceil() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int
rule low(s E):
    s.x < 2.5: d(s) = Low
rule high(s E):
    s.x >= 2.5: d(s) = High
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 2);
    }

    #[test]
    fn reversed_negative_fractional_thresholds_match_exhaustive_enumeration() {
        let source = r"mod M
enum Result:
    Low
    High
record E:
    x: Int [-5, 5]
rule low(s E):
    -1.5 > s.x: d(s) = Low
rule high(s E):
    -1.5 <= s.x: d(s) = High
assert total(s E):
    d(s)
";
        let exhaustive = raw_counterexamples(source);
        let partitioned = analyze_text(source, 10);
        assert!(exhaustive.is_empty());
        assert_eq!(partitioned.verdict, AnalysisVerdict::Passed);
        assert_eq!(partitioned.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(partitioned.planned_evaluations, 2);
    }

    #[test]
    fn arithmetic_input_expression_falls_back_to_inconclusive_sampling() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 1_000_000_000]
rule low(s E):
    s.x + 1 < 50: d(s) = Low
rule high(s E):
    s.x + 1 >= 50: d(s) = High
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("arithmetic"))
        );
        let report = AnalysisReport {
            invariants: vec![invariant],
            findings: Vec::new(),
        };
        let text = report.render_text();
        assert!(text.contains("? total\n  inconclusive ·"));
        assert!(text.contains("boundary samples checked · not exhaustive"));
        assert!(text.contains("  reason ·"));
    }

    #[test]
    fn derive_condition_falls_back_to_inconclusive_sampling() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 1_000_000_000]
fn shifted(s E) Int:
    s.x + 1
rule low(s E):
    shifted(s) < 50: d(s) = Low
rule high(s E):
    shifted(s) >= 50: d(s) = High
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("an `fn` call"))
        );
    }

    #[test]
    fn representative_region_limit_is_truncated_not_proved() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Low
    Exact
    High
record E:
    x: Int [0, 1_000_000_000]
rule low(s E):
    s.x < 50: d(s) = Low
rule exact(s E):
    s.x = 50: d(s) = Exact
rule high(s E):
    s.x > 50: d(s) = High
assert total(s E):
    d(s)
",
            2,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.evaluated, 2);
        assert_eq!(invariant.planned_evaluations, 3);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("exact threshold partition"))
        );
    }

    #[test]
    fn counterexample_limit_stops_early_and_reports_truncation() {
        let program = compile_text(
            r"mod M
record E:
    x: Int [0, 2]
rule unavailable(e E):
    e.x < 0: d(e) = O
assert total(e E):
    e.x = 1 | e.x != 1: d(e) = O
",
        );
        let report = analyze_with_solver(
            &program,
            Some("total"),
            &AnalysisOptions {
                max_evaluations: 100,
                max_counterexamples: 1,
            },
            SolverMode::Off,
        );
        let invariant = &report.invariants[0];
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.evaluated, 1);
        assert!(invariant.planned_evaluations > invariant.evaluated);
        assert_eq!(invariant.counterexamples.len(), 1);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note == "stopped after 1 counterexample(s)")
        );
    }

    #[test]
    fn threshold_partition_matches_exhaustive_gap_witness_on_small_range() {
        let source = r"mod M
enum Result:
    Low
    High
record E:
    x: Int [0, 10]
rule low(s E):
    s.x < 5: d(s) = Low
rule high(s E):
    s.x > 5: d(s) = High
assert total(s E):
    d(s)
";
        let exhaustive = raw_counterexamples(source);
        let partitioned = analyze_text(source, 10);
        assert_eq!(partitioned.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(partitioned.verdict, AnalysisVerdict::Failed);
        assert_eq!(exhaustive[0].input, partitioned.counterexamples[0].input);
    }

    #[test]
    fn empty_resolved_value_set_is_reported_as_undefined() {
        let invariant = analyze_text(
            r"mod M
record E:
    x: Int [0, 0]
rule no_result(s E):
    s.x < s.x: d(s) = O
assert optional_contract(s E):
    d(s)?
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
    }

    #[test]
    fn decimal_boundary_sampling_does_not_overflow_at_maximum() {
        let field = FieldDecl {
            name: Spanned::new("x".into(), Span::default()),
            ty: TypeRef::Decimal,
            ty_span: Span::default(),
            range: None,
            domain: None,
            optional: false,
            span: Span::default(),
        };
        let values = decimal_values(&field, &BTreeSet::from([Decimal::MAX]));
        assert!(values.contains(&Value::decimal(Decimal::MAX)));
    }

    #[test]
    fn full_i64_range_size_is_not_saturated_into_a_false_finite_size() {
        let entity = EntityDecl {
            name: Spanned::new("E".into(), Span::default()),
            fields: vec![FieldDecl {
                name: Spanned::new("x".into(), Span::default()),
                ty: TypeRef::Int,
                ty_span: Span::default(),
                range: Some(RangeConstraint {
                    start: NumericLiteral::Int(i64::MIN),
                    end: NumericLiteral::Int(i64::MAX),
                    start_inclusive: true,
                    end_inclusive: true,
                    span: Span::default(),
                }),
                domain: None,
                optional: false,
                span: Span::default(),
            }],
            span: Span::default(),
        };
        let program = crate::compile_source(SourceFile::new(
            "empty.tes",
            "mod M\nrecord E:\n    x: Int\n",
        ))
        .program
        .expect("compiled program");
        assert_eq!(finite_domain_size(&program, &entity), None);
    }

    #[test]
    fn equality_at_i64_max_partitions_the_full_integer_domain_without_overflow() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Other
    Maximum
record E:
    x: Int
rule maximum(s E):
    s.x = 9_223_372_036_854_775_807: d(s) = Maximum
rule other(s E):
    s.x != 9_223_372_036_854_775_807: d(s) = Other
assert total(s E):
    d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 2);
    }

    #[test]
    fn huge_requested_limit_uses_partition_instead_of_materializing_a_huge_int_vec() {
        let invariant = analyze_text(
            r"mod M
enum Result:
    Negative
    Nonnegative
record E:
    x: Int [-9_000_000_000_000_000_000, 9_000_000_000_000_000_000]
rule negative(s E):
    s.x < 0: d(s) = Negative
rule nonnegative(s E):
    s.x >= 0: d(s) = Nonnegative
assert total(s E):
    d(s)
",
            usize::MAX,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("internal safety cap"))
        );
    }

    #[test]
    fn threshold_completeness_has_stable_serde_name() {
        assert_eq!(
            serde_json::to_value(Completeness::ThresholdPartitioned).unwrap(),
            serde_json::json!("threshold_partitioned")
        );
    }
}