Currently when we compile rational literals to SMTLib we simply cast the Rational value back to a double and then print the result. Unfortunately this obviously runs into floating point precision issues, and e.g. in andGate.vnnlib we currently end up with -3.1365920000000003 rather than -3.136592.
The right way to do this is to distinguish between rational and floating point literals in the frontend (e.g. 1.31 and 1.31f) and then make a similar distinction in SMTLib (which also supports that).
Currently when we compile rational literals to SMTLib we simply cast the
Rational
value back to adouble
and then print the result. Unfortunately this obviously runs into floating point precision issues, and e.g. inandGate.vnnlib
we currently end up with-3.1365920000000003
rather than-3.136592
.The right way to do this is to distinguish between rational and floating point literals in the frontend (e.g. 1.31 and 1.31f) and then make a similar distinction in SMTLib (which also supports that).