Global constant missing in the RAC evaluation context
In the test , the verdict for the CE for the goal g2_lab
is incomplete because the postcondition of the goal cannot be evaluated by the RAC.
The model for the CE contains a value for g
and for x
, but the evaluation context in the RAC does not contain any value for the global constant g
(use --debug=rac-values
).