Module symbolic_analysis 

Symbolic value definitions and Z3-backed proof helpers. Symbolic value domain and Z3 proof adapter for Senryx.

The path visitor records lightweight symbolic definitions for MIR locals. Property checkers translate those definitions plus path constraints into Z3 bit-vector formulas and prove obligations by checking that the negation is unsatisfiable.

Structs

ValueDomain

Current symbolic value information for one MIR local.

Enums

AnaOperand

Operand used inside symbolic definitions.

SymbolicDef

Symbolic definition tracked for one MIR local.

Functions

binop_to_str 🔒

debug_z3_solver_state 🔒

get_operand_bv 🔒

operand_to_str 🔒

verify_with_z3

Verifies a target property using Z3 SMT solver given variable domains and path constraints. Returns true if the property holds (UNSAT for negation), false otherwise.