import type { AnalysisContext, Finding, ModuleRecord } from "./types.js";
/**
 * Layer 3: SMT Constraint Solver
 * Uses Z3 to prove path unreachability in complex logical branches.
 */
export declare function analyzeLayer3(context: AnalysisContext): Promise<Finding[]>;
export declare function encodePredicate(node: any, z3: any, solver?: any, module?: ModuleRecord, bindings?: Map<string, any>): any;