Since recently, calls to val-functions are executed abstractly, also in concrete execution. This means that the result of the call is just the result value from the model, if the model provides it, or the default value otherwise.
Default values are a shot in the dark regarding the postconditions, which are then likely to be wrong. A contradiction in the postcondition of an abstract call results in the RAC execution to get stuck, which results in the final verdict that the model is BAD, and the prover model is hidden.
RAC execution and the final verdict should in this case be INCOMPLETE, because it is an incompleteness of the program (missing implementation) and the model (missing value). The prover model should be retained.
With this MR, all values track their origin (from a computation, from the model, default value), and when an assumption is disproven, an exception Cannot_compute is raised instead of an exception RAC_stuck.