Cubicle 1.1.2 documentation and source : Safety.check

let check s n =
  (*Debug.unsafe s;*)
  try
    if not (obviously_safe s n) then
      begin
	Prover.unsafe s n;
	if not quiet then eprintf "\nUnsafe trace: @[%a@]@."
				  Node.print_history n;
        raise (Unsafe n)
      end
  with
    | Smt.Unsat _ -> ()