Skip to main content

new_solver

synth_verify::solver

Function new_solver 

Source 
pub fn new_solver() -> Box<dyn BvSolver>
Expand description

Construct the configured solver:

  • default: OrdealSolver;
  • with the z3-solver feature compiled in and SYNTH_SOLVER_DIFF=1: the differential solver (ordeal checked against Z3 on every query).