Module Symex.Solver_result

type t =
  1. | Sat
    (*

    The formula is satisfiable

    *)
  2. | Unsat
    (*

    The formula is unsatisfiable

    *)
  3. | Unknown
    (*

    Satisfiability could not be determined (e.g. due to a timeout)

    *)
val pp : Format.formatter -> t -> unit
val is_sat : t -> bool
val is_unsat : t -> bool
val admissible : mode:Approx.t -> t -> bool

admissible ~mode result determines whether a branch should be taken based on the solver result and approximation mode.

The decision matrix:

  • Sat, _: Always take the branch (definitely feasible)
  • Unsat, _: Never take the branch (definitely infeasible)
  • Unknown, OX: Take the branch (over-approximate: don't miss paths)
  • Unknown, UX: Don't take the branch (under-approximate: avoid possibly unsatisfiable paths)