Check_ce: simplify API interface

All functions in Check_ce now assume that counterexample checking has been requested. Two entry functions are provided, to request both small and giant step RAC (useful for checking WhyML programs) or to only request giant step RAC (useful when the small-step will be performed on another language). The RAC log is returned, and should be interpreted to produce a counterexample. As a temporary helper, an incomplete model is also returned, that contains all the values extracted from the log.