What is the semantics of gWhys icons?
The meaning of the icons is the following: valid (green dot): the VC is a true formula invalid (red dot): the VC is not a true formula. In principle, invalid should be identified with unknown, because provers can very rarely say that a formula is definitely not true. Historically, Simplify answers is either valid or invalid, where invalid indeed means unknown. The GWhy maps those invalid to the question mark but the textual output might still classified them as invalid. unknown (question mark) : it is not known if the formula is true or not timeout (scissor): the prover did not answer before the timeout (10 s by default) failure (tools): the prover answer was not recognized. Failure might have many causes: failure to run the prover’s process, a syntax error in the output file, etc. In case of failure, one can inspect the problem by activating debug (menu Proof/Debug mode) and look at the debugging output in the console. (hard disk): this VC is already known valid in GWhy cache. Note th
