diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index b3c691fb..1b6efa46 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1243,7 +1243,7 @@ let prove_z3 env (NC_aux (_, l) as nc) = | Constraint.Sat -> typ_debug (lazy "sat"); false | Constraint.Unknown -> typ_debug (lazy "unknown"); false -let solve env (Nexp_aux (_, l) as nexp) = +let solve env (Nexp_aux (_, l) as nexp) = typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_nexp nexp ^ " = ?")); match nexp with @@ -1255,6 +1255,8 @@ let solve env (Nexp_aux (_, l) as nexp) = let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in Constraint.solve_z3 l vars constr (mk_kid "solve#") + + let prove env nc = typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); let (NC_aux (nc_aux, _) as nc) = Env.expand_constraint_synonyms env nc in |