Normalise presentation of counterexample values for records
We often have differences in bench for counterexample due to apparently two ways of presenting values for records, depending whether they have only one field or several. This is examplified in the diff for a recent nightly bench:
- {"proj_name": "length",
- "type": "Proj",
- "value": {"type": "Integer", "val": "0"}}
+ {"type": "Record",
+ "val":
+ {"Field":
+ [{"field": "elts",
+ "value":
+ {"type": "Array",
+ "val": [{"others": {"type": "Integer", "val": "1"}}]}},
+ {"field": "length", "value": {"type": "Integer", "val": "0"}}]}}
I suggest to never choose the first presentation, with Proj
instead of Record
. This may impact the presentation of values for machines integers, but we could investigate that afterwards.
Generally speaking, the presentation of a record value should be decided in function of the Why3 type of this record, not be an heuristics on the produced value: in other words, it is not because the solver returns a value for only one field of the record that the presentation of the value should be changed.
Moreover, the presentation may be adapted for types that we know specifically : machine integers, arrays.