This PR fixes two issues related with the serialization of MInts in the proof trace:
We add support for parametric sorts in the KORE rich header generation algorithm, because MInt sorts are indeed parametric. To do that we need to have an invariant of topological sorting of the ordinals of sorts, i.e. every sort needs to have an ordinal greater than the ordinals of all its parameters. We can guarantee that by generating the sort ordinals in this way, since all parametric sorts are known statically at compile time.
We fix a bug on how we pass arguments to the emit_*_to_proof_trace functions that emit various events to the proof trace. Previously, when these functions needed to emit a KORE term as part of an event, they would accept a pointer to said KORE term as argument, an in case the term was a boolean or machine integer, that pointer would be cast to the actual value. However for machine integers longer than 64 bits, the pointer data type (which is 64 bit long) is not enough to store the machine integer value. We fix this by passing an actual pointer to the machine integer value in the case where the machine integer is longer than 64 bits.
This PR fixes two issues related with the serialization of MInts in the proof trace:
emit_*_to_proof_trace
functions that emit various events to the proof trace. Previously, when these functions needed to emit a KORE term as part of an event, they would accept a pointer to said KORE term as argument, an in case the term was a boolean or machine integer, that pointer would be cast to the actual value. However for machine integers longer than 64 bits, the pointer data type (which is 64 bit long) is not enough to store the machine integer value. We fix this by passing an actual pointer to the machine integer value in the case where the machine integer is longer than 64 bits.