pub type Z3_goal = *mut _Z3_goal;
Set of formulas that can be solved and/or transformed using tactics and solvers.