SVF Python Z3 API

Z3Mgr API Documentation

Method	Description
`getZ3Expr(var_id: int, ctx)`	Retrieves the Z3 expression for a given variable ID within a context.
`getZ3Val(value)`	Converts a value to a Z3 value.
`addToSolver(expr)`	Adds an expression to the Z3 solver.
`solver.push()`	Pushes a context onto the solver stack.
`solver.pop()`	Pops a context from the solver stack.
`solver.check()`	Checks the satisfiability of the current solver context.
`getMemObjAddress(var_id: int)`	Retrieves the memory object address for a given variable ID.
`loadValue(expr)`	Loads a value from a given Z3 expression.
`storeValue(lhs, rhs)`	Stores a value into a location.
`getGepOffset(stmt, ctx)`	Retrieves the offset for a GEP statement.
`getGepObjAddress(rhs, offset)`	Retrieves the address for a GEP object with a given offset.