Logic QF_LIRA is not supported

[jhoenicke]

Even though there is no official QF_LIRA logic definition on the SMT-LIB website, there are some benchmarks using this logic.

1166: UserWarning: Unknown logic 'QF_LIRA'. Ignoring set-logic command.

[marcogario]

:wave: Thanks for reporting this.

What is the behavior you expect here?

Since the logic is not officially part of the SMT-LIB, we need to understand what to do when talking to solvers.

I would expect that you are still able to call the solver (as I think this is just really a warning), and in the worst case detecting the logic as QF_URLIRA. If this is blocking you, please let me know more about your use case.

[jhoenicke]

Although there is no formal logic description for QF_LIRA, there are official SMT-LIB benchmarks using this logic listed on http://smtlib.cs.uiowa.edu/benchmarks.shtml

This is similar to QF_ALIA, which also have no formal logic description on http://smtlib.cs.uiowa.edu/logics.shtml

So most backend solvers should already support QF_LIRA.

My application is to extend the model-validation track from SMT-COMP to other logics and it is working fine, except for this warning (which screws up the evaluation scripts). This model-validation just uses the built-in simplifier (if the asserted formulas simplify to true, the model is validated).

[marcogario]

Thanks for the feedback. I would accept a patch to extend the set of logics to include these cases, if you think you can submit one.

In the meanwhile, you should be able to disable the user warning from the command line (python -W ignore should be sufficient) or from the top-level module

import warnings
warnings.filterwarnings("ignore")