SMT-RAT submission

[ValentinPromies]

No description provided.

[github-actions]

Summary of modified submissions

SMT-RAT

• 3 authors
• website: https://github.com/ths-rwth/smtrat
• Participations
  • SingleQuery
    • Arith
      • NRA
    • QF_NonLinearRealArith
      • all
  • ModelValidation
    • QF_NonLinearRealArith
      • all

[martinjonas]

@ValentinPromies We have executed the latest version of SMT-RAT on a randomly chosen subset of 20 single-query benchmarks from each logic where it participates. The benchmarks are also scrambled by the competition scrambler (with seed 1). You can find the results here: https://www.fi.muni.cz/~xjonas/smtcomp/smtrat.table.html#/table

Quick explanation:

• Green status means that the result agrees with the (set-info :status _) annotation from the benchmark.
• Blue status means that the benchmark has annotation (set-info :status unknown).
• By clicking on the result (e.g. false, true, ABORTED, …) you can see the command-line arguments with which your solver was called and its output on the benchmark.
• By clicking on the benchmark name (i.e., *scrambled*.yml), you can see the details of the benchmark including its contents (by clicking on the file link in input_files) and the name of the original bennchmark before scrambling (e.g., # original_files: 'non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2').

Please check whether there are some discrepancies, such as missing/extra logics, unexpected aborts or unknowns, and similar. If you update the solver, let me know and I can execute further test runs. We still have plenty of time for several follow-up test runs.

[martinjonas]

@ValentinPromies We have finished test runs of model-validation track. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/smtrat_model.table.html#/table

As before, you can click on the status of the benchmark to see the output of your solver. If you find any discrepancies or extra/missing logics, please let me know.

Note that we selected only SAT benchmarks for model validation. As a result of that, some logics do not contain any benchmarks. So do not be surprised if you have subscribed to one of these logics and you do not have any result for it. In particular, the logics are: QF_UFFP, QF_UFBVDT, QF_UFDTNIA, QF_NIRA.

[ValentinPromies]

@martinjonas we updated our solver. Can you please run the tests again? Thanks for the help!

[martinjonas]

@martinjonas we updated our solver. Can you please run the tests again? Thanks for the help!

Sure, done! You can find the new results on the same webpage as before. I reran both single-query and model-validation tracks.