tessellate-core 0.3.0

use crate::ast::{
    BinaryOp, Declaration, Effect, Expr, ExprKind, FieldDecl, InvariantAssertion, InvariantDecl,
    InvariantQuantifier, Literal, NumericLiteral, RuleDecl, TypeRef,
};
use crate::compiler::{CompiledProgram, 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>,
    #[serde(default, skip_serializing_if = "Vec::is_empty")]
    pub traces: Vec<crate::trace::TraceAnalysis>,
    pub findings: Vec<StaticFinding>,
}

impl AnalysisReport {
    #[must_use]
    pub fn success(&self) -> bool {
        (!self.invariants.is_empty() || !self.traces.is_empty())
            && self
                .invariants
                .iter()
                .all(|invariant| invariant.verdict == AnalysisVerdict::Passed)
            && self
                .traces
                .iter()
                .all(|trace| trace.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() || !self.traces.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}");
                    }
                }
            }
        }
        for (trace_index, trace) in self.traces.iter().enumerate() {
            if !self.invariants.is_empty() || trace_index > 0 {
                out.push('\n');
            }
            out.push_str(&trace.render_text());
        }
        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(),
        traces: if selected_invariant.is_none() {
            crate::trace::analyze_traces(program, None, options)
        } else {
            Vec::new()
        },
        findings: static_findings(program),
    }
}

fn analyze_invariant(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    options: &AnalysisOptions,
    solver_mode: SolverMode,
) -> InvariantAnalysis {
    if invariant.variables.is_empty() {
        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!["an assertion must declare at least one record parameter".into()],
        };
    }
    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 expected = match constant_value(program, &expectation.value, 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 is false".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. A false 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)
                || matches!(&rule.effect, Effect::Override { rule, .. }
                        if candidate_rule_names.contains(&normalize_name(&rule.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)?;
        inspector.require_constant(
            &expectation.value,
            &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));
    };
    let (NumericLiteral::Int(start), NumericLiteral::Int(end)) = (&range.start, &range.end) else {
        return Err(format!(
            "Int field `{}` has non-integer range bounds",
            field.name.value
        ));
    };
    Ok((*start, *end))
}

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(|range| numeric_decimal(&range.start))
                .unwrap_or(Decimal::ZERO);
            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 (NumericLiteral::Int(start), NumericLiteral::Int(end)) =
                        (&range.start, &range.end)
                    else {
                        return None;
                    };
                    if start > end {
                        return None;
                    }
                    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 (NumericLiteral::Int(start), NumericLiteral::Int(end)) =
                        (&range.start, &range.end)
                    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(|range| {
        let (NumericLiteral::Int(start), NumericLiteral::Int(end)) = (&range.start, &range.end)
        else {
            return None;
        };
        Some((*start, *end))
    });
    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(|range| Some((numeric_decimal(&range.start)?, numeric_decimal(&range.end)?)));
    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::Enum(_)
            | Declaration::Entity(_)
            | Declaration::State(_)
            | Declaration::Decision(_)
            | Declaration::Action(_) => {}
            Declaration::Transition(value) => {
                collect_expr_numbers(&value.condition, &mut constants);
                for update in &value.updates {
                    collect_expr_numbers(&update.value, &mut constants);
                }
            }
            Declaration::Trace(value) => {
                collect_expr_numbers(&value.initial, &mut constants);
                for condition in &value.always {
                    collect_expr_numbers(condition, &mut constants);
                }
                if let Some(condition) = &value.terminal {
                    collect_expr_numbers(condition, &mut constants);
                }
            }
            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);
                    collect_expr_numbers(&expectation.value, &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 {
                produced
                    .entry(enum_name.clone())
                    .or_default()
                    .insert(variant.clone());
            } 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(&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

dec result(request Request) -> Result

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

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

    rule no(request Request):
        not request.enabled => result(request) = No
",
        );
        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")
    }

    /// 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,
            range: Some(RangeConstraint {
                start: NumericLiteral::Int(0),
                end: NumericLiteral::Int(3),
                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 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(),
            }],
            traces: 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()],
                ),
            ],
            traces: Vec::new(),
            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
dec d(e E) -> Result
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],
            traces: Vec::new(),
            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
dec d(e E) -> Result
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],
            traces: Vec::new(),
            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
dec d(e E) -> Result
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
dec d(left Left, right Right) -> Result
rule yes(left Left, right Right):
    left.enabled and 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
dec d(e E) -> Result
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 is false"
        );
    }

    #[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
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(s E) -> Result
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],
            traces: Vec::new(),
            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
dec d(s E) -> Result
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
dec d(s E) -> Result
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
dec d(s E) -> Result
rule yes_a(s E):
    s.flag and s.mode = A => d(s) = Yes
rule yes_b(s E):
    s.flag and s.mode = B => d(s) = Yes
rule no_a(s E):
    not s.flag and s.mode = A => d(s) = No
rule no_b(s E):
    not s.flag and 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
dec d(s E) -> Result
dec unrelated(s E) -> Bool
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) = true
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
dec d(s E) -> Result
rule base(s E):
    true => 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
dec d(s E) -> Result
rule base(s E):
    true => 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
dec d(first E, second E) -> Result
rule yes(left E, right E):
    left.value < 50 and 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
dec d(first E, second E) -> Result
rule swapped(left E, right E):
    left.x = 2 and 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
dec d(first E, second E) -> Result
rule ll(left E, right E):
    left.x < 50 and right.x < 100 => d(left, right) = LL
rule lh(left E, right E):
    left.x < 50 and right.x >= 100 => d(left, right) = LH
rule hl(left E, right E):
    left.x >= 50 and right.x < 100 => d(left, right) = HL
rule hh(left E, right E):
    left.x >= 50 and 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
dec d(first E, second E) -> Result
rule ll(left E, right E):
    left.x < 50 and right.x < 100 => d(left, right) = LL
rule lh(left E, right E):
    left.x < 50 and right.x >= 100 => d(left, right) = LH
rule hl(left E, right E):
    left.x >= 50 and 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
dec d(first E, second E) -> Result
rule yes(left E, right E):
    left.x < 100 and 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
dec d(order Order, member Member) -> Result
rule premium(order Order, member Member):
    member.premium => d(order, member) = Free
rule large(order Order, member Member):
    not member.premium and order.amount >= 50 => d(order, member) = Free
rule small(order Order, member Member):
    not member.premium and 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
dec d(order Order) -> Result
rule free(order Order):
    true => d(order) = Free
assert total(o Order, c Customer):
    c.vip and 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
dec d(first E, second E) -> Result
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
dec d(order Order, coupon Coupon) -> Result
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
dec d(order Order, coupon Coupon) -> Result
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
dec d(a A, b B) -> Result
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
dec d(a A, b B) -> Result
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
dec d(order Order, customer Customer) -> Result
rule preferred(order Order, customer Customer):
    customer.premium and customer.tier = Preferred => d(order, customer) = Free
rule amount(order Order, customer Customer):
    not customer.premium and 2 * order.amount - customer.credit >= 50_000 => d(order, customer) = Free
rule paid(order Order, customer Customer):
    not customer.premium and 2 * order.amount - customer.credit < 50_000 => d(order, customer) = Paid
rule standard_premium(order Order, customer Customer):
    customer.premium and customer.tier = Standard => d(order, customer) = Paid
assert total(order Order, customer Customer):
    customer.premium and 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
dec audit(e Expense) -> Result
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
dec classify(q Quote) -> Result
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
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(order Order, coupon Coupon) -> Result
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)
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(e E) -> Result
rule skipped_left_false(e E):
    false and e.x / 0 > 0 => d(e) = Any
rule skipped_right_false(e E):
    e.x / 0 > 0 and false => d(e) = Any
rule applied_left_true(e E):
    true or e.x / 0 > 0 => d(e) = Any
rule applied_right_true(e E):
    e.x / 0 > 0 or true => 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
dec d(e E) -> Result
rule any(e E):
    true => 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
dec d(e E) -> Decimal
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
dec d(e E) -> Decimal
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
dec d(e E) -> Decimal
rule copy(e E):
    true => 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
dec d(e E) -> Bool
rule first(e E):
    e.guard or not e.guard => d(e) = e.value
rule second(e E):
    not e.guard or e.guard => d(e) = not not e.value
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
dec d(e E) -> Bool
rule first(e E):
    e.guard or not e.guard => d(e) = e.value
rule second(e E):
    not e.guard or e.guard => d(e) = not e.value
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
dec d(e E) -> Int
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
dec d(e E) -> Int
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
dec d(e E) -> Int
rule increment(e E):
    true => 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
dec d(e E) -> Int
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
dec d(e E) -> Int*
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
dec d(e E) -> Int*
rule overflow(e E):
    true => 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
dec d(e E) -> Result
rule mode_a(e E):
    e.mode = A => d(e) = Covered
rule disabled_b(e E):
    not e.enabled and 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))
dec d(order Order, coupon Coupon) -> Result
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))
dec d(order Order, coupon Coupon) -> Result
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)
dec d(left Point, right Point) -> Result
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)
dec d(left Point, right Point) -> Result
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}
dec d(e E) -> Result
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)
dec d(e E) -> Result
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
dec d(a A, b B) -> Result
rule base(a A, b B):
    true => 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
dec d(a E, b E) -> Result
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
dec d(left E, right E) -> Result
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
dec d(left E, right E) -> Result
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?
dec d(e E) -> Bool
rule present(e E):
    e.maybe => d(e) = true
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
dec d(e E) -> Result
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
dec d(e E) -> Result
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
dec d(e E) -> Result
rule any(e E):
    (e.b0 or not e.b0) and (e.b1 or not e.b1) and (e.b2 or not e.b2) and (e.b3 or not e.b3) and (e.b4 or not e.b4) and (e.b5 or not e.b5) and (e.b6 or not e.b6) and (e.b7 or not e.b7) and (e.b8 or not e.b8) and (e.b9 or not e.b9) and (e.b10 or not e.b10) => 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
dec d(e E) -> Result
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
dec d(e E) -> Result
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}
dec d(e E) -> Result
rule draft(e E):
    e.status = "draft" and e.rate >= 0.05 => d(e) = Draft
rule approved(e E):
    e.status = "approved" and 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
dec d(e E) -> Result
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)
dec shipping(o Order) -> Result
rule normal_free(o Order):
    payable(o) >= 50 and not o.remote => shipping(o) = Free
rule normal_paid(o Order):
    payable(o) < 50 and not o.remote => shipping(o) = Paid
rule remote_paid(o Order):
    o.remote => shipping(o) = Paid
rule approved_remote(o Order):
    o.remote and o.approved and payable(o) >= 50 => shipping(o) = Free
rule approved_remote_override(o Order):
    o.remote and o.approved and payable(o) >= 50 => 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
dec d(a E, b E) -> Result
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
dec d(query Query) -> Result
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):
    true => 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
dec d(query Query) -> Result
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):
    true => 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
dec d(first E, second E) -> Result
rule present(left E, right E):
    left.x != 1 or 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
dec d(s E) -> Result
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?
dec d(s E) -> Result
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
dec d(s E) -> Result
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
dec d(s E) -> Result
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
dec d(s E) -> Result
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],
            traces: Vec::new(),
            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
dec d(s E) -> Result
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
dec d(s E) -> Result
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
dec d(e E) -> Bool
assert total(e E):
    e.x = 1 or e.x != 1 => d(e) = true
",
        );
        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
dec d(s E) -> Result
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
dec d(s E) -> Bool?
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,
            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,
                range: Some(RangeConstraint {
                    start: NumericLiteral::Int(i64::MIN),
                    end: NumericLiteral::Int(i64::MAX),
                    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
dec d(s E) -> Result
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
dec d(s E) -> Result
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")
        );
    }
}