Function prove 

pub fn prove(
    z3: &mut Z3,
    facts: &[Constraint],
    goal: &Constraint,
    nonneg: &[Var],
) -> bool

Try to prove nonlinear goal from facts.