Create iProver

[konstantin-korovin]

iProver v3.9.3 initial submission

[martinjonas]

@konstantin-korovin Thanks for the submission! Can you please change the name of the submission file iprover to iprover.json? All our scripts and the continuous integration rely on the file extension.

[konstantin-korovin]

@ma

Done.
Thanks.

@konstantin-korovin Thanks for the submission! Can you please change the name of the submission file iprover to iprover.json? All our scripts and the continuous integration rely on the file extension.

[github-actions]

Summary of modified submissions

iProver v3.9.3

• 1 authors
• website: https://gitlab.com/korovin/iprover
• Participations
  • SingleQuery
    • Arith
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+NonLinearArith
      • all
  • Parallel
    • Arith
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+NonLinearArith
      • all

[konstantin-korovin]

Just to note that some tests are failed due to iProver returning "unknown" in sat cases. which is expected as it is targeted towards unsat, apart from UF.

[konstantin-korovin]

@wintered I updated the link, thanks!

[martinjonas]

@konstantin-korovin Thanks for submitting iProver to this year's SMT-COMP!

We have executed your solver on a small number of benchmarks from each logic it should compete in (except the parallel track). You can find the results here:

• Single Query Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/iproverv393.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks).

You can check whether all the results we have obtained are expected. If not, please let us know here.

Some notes:

• We have used less resources than will be used in the final runs.
• The benchmarks are scrambled by the official scrambler with seed 1.
• The column status shows whether your solver decided the benchmark as sat (true) or unsat (false).
• You can click on the value in the status column to see the output of your solver on that benchmark.

If you upload a new version of the solver and want to have another test run, let me know. We still have some time for that.

Happy rest of the competition!
Martin

[martinjonas]

@konstantin-korovin I was going to run also test runs for the Parallel track, but unfortunately it seems that iProver is the only solver that participates in quantified divisions of the Parallel track. So the divisions are going to be non-competitive.

If you want the results just for your information, let me know and I will run them.

[konstantin-korovin]

@konstantin-korovin I was going to run also test runs for the Parallel track, but unfortunately it seems that iProver is the only solver that participates in quantified divisions of the Parallel track. So the divisions are going to be non-competitive.

If you want the results just for your information, let me know and I will run them.

Thanks @martinjonas! it is a pity that no other system was submitted for the quantified parallel track, hopefully next time will be different. Many thanks for the offer to run iProver but let's skip it in this iteration.