Support for theory combination of reals and integers

[daniel-larraz]

Hello,

Congratulations for the great work. Do you have plans for supporting the theory combination of reals and integers?

Thank you,
Daniel

[blishko]

Hi Daniel,

Thank you! Support for LIRA would be good to have, but currently is relatively low on our long TODO list, as we don't have any immediate application for it.
Do you have any particular use case in mind? That could move this particular feature higher on the list.

Cheers,
Martin

[daniel-larraz]

We are considering supporting OpenSMT as a back-end solver in the Kind 2 model checker, especially because of its good support for generating interpolants. However, we often find model checking problems that contain reals and integers, so having support for LIRA would be great.

Cheers,
Daniel

[blishko]

Interesting! Do you get mixed arithmetic problems from Lustre programs?
So, for LIRA, you would need not only solving, but also interpolation, right? My guess is that it would require non-trivial amount of work. We don't have the capacity to work on it at the moment, but I will keep it in mind and try to find someone to work on this.

[daniel-larraz]

Yes, that's right. We get mixed arithmetic problems from Lustre programs. We would need interpolation too.
I'm sure the Software Verification community would appreciate having this feature.

Thank you for your feedback and consideration.