search

usi-verification-and-security / opensmt

The opensmt solver
Other
76 stars 18 forks source link

OsmtInternalException: Mode not supported for QF_UFLRA yet #605

Open daniel-larraz opened 1 year ago

daniel-larraz commented 1 year ago

OpenSMT v2.5.0 terminates with an error when solving this SMTLIB script.

Output:

[...]
terminate called after throwing an instance of 'OsmtInternalException'
  what():  Mode not supported for QF_UFLRA yet
Aborted (core dumped)

OS: Ubuntu 20.04

blishko commented 1 year ago

Hi @daniel-larraz! Unfortunately, Interpolation is not supported for the combination of theories yet. This is a priority, but it will require substantial amount of work. I will let you know when this is supported.

daniel-larraz commented 1 year ago

Sorry, I had forgotten that interpolation is not supported for any combination of theories. For a moment I thought the support was not available only for QF_LIRA.

Thank you.