pub type Z3_solver = *mut _Z3_solver;
(Incremental) solver, possibly specialized by a particular tactic or logic.