Updates to the retrieving model results in wp

[fortunac]

• We should refactor getting a model from the solver to it's own function as there are instances of

 let model = Z3.Solver.get_model solver
              |> Option.value_exn ?here:None ?error:None ?message:None

in constraint.ml, output.ml, precondition.ml, and test_precondition.ml. We should also add a more useful error message for the failure case.

• When returning the result of SAT or UNSAT, in
  

  cbat_tools/wp/lib/bap_wp/src/precondition.ml

  Line 887 in aca7ac6

  let check ?refute:(refute = true) (solver : Z3.Solver.solver) (ctx : Z3.context)

  
  we should return either UNSAT or SAT with a model atomically, possibly by creating our own data type that would mirror an option.