Draft PR for instrumenting the invoked function's return value into the env.
Since the return value may be (), the plan is to use the Apalache option type.
However, the required operators are not loaded by default, and would need to be injected into the JSON IR.
Also, we would have likely have to annotate the env record field with an appropriate type.
Draft PR for instrumenting the invoked function's return value into the env.
Since the return value may be
(), the plan is to use the Apalache option type. However, the required operators are not loaded by default, and would need to be injected into the JSON IR.Also, we would have likely have to annotate the env record field with an appropriate type.
Closes #88