Module z3

This module contains glue code that implements liblisa::smt::SmtSolver. To use this module, the feature z3 needs to be enabled.

Structs

• BV
  A Z3 bitvector.
• Bool
  A Z3 Bool.
• BvArray
  A Z3 Array.
• Int
  A Z3 Int.
• Model
  The Z3 model returned when assertions are satisfiable.
• ModelRef
  A reference to the Z3 model returned when assertions are satisfiable.
• ThreadLocalZ3
  A SolverProvider that uses a thread-local Z3 instance.
• Z3Solver
  The Z3 SmtSolver.