Closed konnov closed 1 year ago
I suspect this is may be happening when deserializing into Apalache's version of the QuintIR. Hopefully we just need to change
to be
- @key("int") case class QuintInt(id: Int, value: Int) extends QuintEx {}
+ @key("int") case class QuintInt(id: Int, value: BigInt) extends QuintEx {}
object QuintInt {
implicit val rw: RW[QuintInt] = macroRW
}
thanks to upickle's support for BigInt
s.
Wow, thanks for the pointer!
This kind of deserialization looks highly optimistic on unpickle's end though. @shonfeder is there a way to make upickle throw instead of just truncating numbers?
Well, I changed it to BigInt
and got this grandiose error message from upickle:
> Input was not a valid representation of the QuintIR: expected string got float64 at index -1 E@11:54:24.817
The reason is that upickle expects fields that are deserialized to BigInt
to be a string in the JSON.
I will look at what we are currently doing with counterexamples and ITF, to keep things roughly synchronized.
There's this PR on the upickle repo, but it seems it never made it in: https://github.com/com-lihaoyi/upickle/pull/191
Not fixed until we also patch the Quint side
Here is a very simple example:
Run
quint verify
as follows (with the proper ritual of starting the Apalache server first):It's obvious that the translation has converted a big integer to i32 MAX_INT somewhere on the way.