Start conversion of RAC exec log to CE model
This is specifically intended to provide RAC-verified CE models to Spark, where there is no easy way to display execution logs. There might still be changes required for the integration, but I would prefer to tackle them after this basic version has been merged.
This MR also adds
- environment variables
WHY3PRINTORIGINALMODEL
andWHY3PRINTDERIVEDMODEL
forwhy3 prove --check-ce
to additionally print the original and derived models for comparison - changes required for the integration of Why3 check-ce to Spark
Edited by Benedikt Becker