Describe the bug
Currently we output scaled steps (as we should) for the --suggest option and the 1.2 branch extended on that concept that we scale steps already as early as reading them. The development release of SPARK fixed the distinction between raw and scaled steps in the JSON output (i.e. check_tree vs. stats object).
Expected Behavior
To prepare for future releases of SPARK, SPAT should be able to detect if step scaling is actually needed and skip the scaling if not. If there is at least one successful proof, we can infer that information from the difference of reported steps in the check_tree array and the corresponding stats object.
Alternatively, we may provide a command line switch to enable scaling or not.
Describe the bug
Currently we output scaled steps (as we should) for the
--suggestoption and the 1.2 branch extended on that concept that we scale steps already as early as reading them. The development release of SPARK fixed the distinction between raw and scaled steps in the JSON output (i.e. check_tree vs. stats object).Expected Behavior
To prepare for future releases of SPARK, SPAT should be able to detect if step scaling is actually needed and skip the scaling if not. If there is at least one successful proof, we can infer that information from the difference of reported steps in the check_tree array and the corresponding stats object.
Alternatively, we may provide a command line switch to enable scaling or not.