Baier D.
Baier D.
> @kfriedberger the SMTLIB2 standard defines the size of an FP as mantissa + exponent with the mantissa including the sign bit. Our current implementation excludes it, and we do...
I now split all changes in regard to FP mantissa into a dedicated [PR here](https://github.com/sosy-lab/java-smt/pull/513). We should first handle that PR, merge it, and then continue here.
Thank you both for your input! I actually like both of your ideas in conjunction! Offer a call like Philipp suggests, and allow the user to specifiy how to handle...
But it is not unspecified, there are just multiple definitions ;D The safest way for us would be to provide a method that forces the user to think about it...
Thanks for reporting! I guess we can keep the current solution until it is fixed. We should however add a `TODO` so that we don't forget which version had the...
Are you sure that the problem is not simply non-linear arithmetic?
My bad, you are correct! The solution you put forward also sounds good!
@kfriedberger i don't know if we want to warn users about the sneaky throws, but it seems reasonable. What do you think?
> Except for the iterator interface in model class, and maybe due to backard compatibility, I do not see any strong reason to hide the exception in the signature. Why...
@PhilippWendler @kfriedberger i updated the PR and the code with explicit exceptions as far as possible. Would you two be so kind and take another look?