Add 20230321-UltimateAutomizerSvcomp2023 benchmarks

[Heizmann]

The dolmen tool still complains about the following.

• Shadowing. Quantified variables have the same identifier than constants that were declared before. I think this is allowed by SMT-LIB.
• Multi-dimensional arrays, i.e., arrays whose sort is (Array (_ BitVec 64) (Array (_ BitVec 64) (_ BitVec 32)))). Arrays of this form are utilized in Ultimate Automizer and supported by various SMT solvers.
• The use of real literals (e.g., 1.0) in FP logics. I think that this is allowed, otherwise one cannot use ((_ to_fp eb sb) RoundingMode Real (_ FloatingPoint eb sb)).
• The use of real division / is FPLRA logics. Seems ok to me as well. Not that each FPLRA utlizes real division only for real literals (e.g., (/ 1.0 2.0). In case this is already allowed in the corresponding FP logics, we can move all FPLRA benchmarks to the corresponding *FP folders.

[mpreiner]

@Heizmann I just enabled CI for this PR. Can you fix the reported errors?

[Heizmann]

Thanks. I constructed the benchmarks in several runs. It looks like I forgot to delete the duplicates in one of the runs. I just fixed that by 3b53df312e89be2c2102e8a25de83ac47dad4524.

[mpreiner]

The use of real literals (e.g., 1.0) in FP logics. I think that this is allowed, otherwise one cannot use ((_ tofp eb sb) RoundingMode Real ( FloatingPoint eb sb)).

The use of real division / is FPLRA logics. Seems ok to me as well. Not that each FPLRA utlizes real division only for real > literals (e.g., (/ 1.0 2.0). In case this is already allowed in the corresponding FP logics, we can move all FPLRA benchmarks to the corresponding *FP folders.

This requires FPLRA.

[mpreiner]

• Shadowing. Quantified variables have the same identifier than constants that were declared before. I think this is allowed by SMT-LIB.
• Multi-dimensional arrays, i.e., arrays whose sort is (Array ( BitVec 64) (Array ( BitVec 64) (_ BitVec 32)))). Arrays of this form are utilized in Ultimate Automizer and supported by various SMT solvers.

Shadowing is fine, dolmen just warns about it in case the user wants to fix it. Multi-dimensional arrays are also fine.

[hansjoergschurr]

Can you add the standard header fields to your :source command? This should look like in the example in the README. The nice description that you included in the benchmarks should stay there, but come after the header. Hence, it should look something like this in your case:

Generated by: Matthias Heizmann
Generated on: 2023-03-21
Generator: Ultimate Automizer
Application: Software verification
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
[...]

(I removed Target Solver since I don't know which solvers Ultimate Automizer typically uses)

[hansjoergschurr]

I used my maintainer super powers to perform the edit ;) and merged the branch now. Thank you for your benchmark submissions. We will run some further checks on our side, but if everything goes well your benchmarks should be included in the next release.

[Heizmann]

@hansjoergschurr Thanks at lot! I postponed this to the weekend, because I have a more pressing deadline in a few hours. Thanks for helping me out.

[Heizmann]

Multi-dimensional arrays are also fine.

@mpreiner Great! I am very happy about this. Multi-dimensional arrays are essential for several tools of our Ultimate framework.

[Heizmann]

(I removed Target Solver since I don't know which solvers Ultimate Automizer typically uses)

Currently, we are utilizing cvc4, cvc5, MathSAT, SMTInterpol, and z3. However, I don't know which solver was involved in producing which script. The concrete solver is also abstracted away by out API. The code that writes the script does not know the name of the solver and it would require some nontrivial refactoring to make this information available.

[hansjoergschurr]

I think then it's indeed the best to not have a Target Solver line.