Submission for smtinterpol

[jhoenicke]

The smtinterpol submission.

[bobot]

Hi @jhoenicke , could you rebase your submission? For simplicity instead of being in the tests, the submission summary is now presented as a specific comment.

[jhoenicke]

@bobot, I'm not sure about the Docker requirement. Is the solver meant to be run with docker run. Because this adds something like 4 seconds overhead just for running solver -version.

Since we have a java application as a portable jar archive, is it okay if our tar.gz submission contains only the jar file and we just assume someone installed java 8 or higher on the path, or do we need to include java in the archive, which is about 300 MB and also architecture specific?

Our docker file is currently just using the public java docker eclipse-tumerin:8 and then copying the jar file and the start script to some directory. Is this what you had in mind?

[mpreiner]

@jhoenicke As far as I understand the Dockerfile is only for building the solver binaries.

[bobot]

The Dockerfile mention were an idea that we forgot to remove in the last iteration of the rules. I'm really sorry . The binaries must already be built. The computers are Ubuntus, we are going to provide the exact name of the image today. I will make an announcement later today.

[mbromber]

JFYI: Your solver link does not seem to work. I get the following error:

Forbidden

You don't have permission to access this resource.

Maybe it is only accessible from your university's intranet?

[jhoenicke]

Fixed. I always have to set permission manually and forgot to set it.

[mbromber]

Thanks. It works now.

[github-actions]

Summary of modified submissions

SMTInterpol

• 14 authors
• website: https://ultimate.informatik.uni-freiburg.de/smtinterpol
• Participations
  • UnsatCore
    • Arith
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+NonLinearArith
      • all
    • QF_Datatypes
      • all
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all
  • SingleQuery
    • Arith
      • all
    • Bitvec
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+MachineArith
      • ABV
      • AUFBV
      • AUFBVDTLIA
      • AUFBVDTNIA
      • AUFBVDTNIRA
      • UFBV
      • UFBVDT
      • UFBVLIA
    • Equality+NonLinearArith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all
  • ModelValidation
    • QF_ADT+BitVec
      • all
    • QF_ADT+LinArith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all
  • Incremental
    • Arith
      • all
    • Bitvec
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+NonLinearArith
      • all
    • QF_Bitvec
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • all
    • QF_Equality+Bitvec+Arith
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all

[martinjonas]

@jhoenicke We have executed the latest version of smtinterpol 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/smtinterpol.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]

@jhoenicke Here are also results of the test run on a small subset of incremental benchmarks: https://www.fi.muni.cz/~xjonas/smtcomp/smtinterpol_inc.table.html#/table

The status column has the following meaning:

• DONE (X correct): the solver terminated successfully and correctly decided X (check-sat) queries before that.
• SOMETHING_ELSE (X correct) (e.g., TIMEOUT (10 correct) or ABORTED (10 correct)): The solver did not terminate successfully, but correctly decided X (check-sat) queries before it crashed or was killed.
• WRONG: There was at least one answer to (check-sat) that did not agree with the status specified in the benchmark.

Again, if there are discrepancies (missing/extra logics, unexpected results), please let me know.

[jhoenicke]

@martinjonas Thanks for the preliminary runs. Do you by any chance already have the error.log files?

[martinjonas]

@martinjonas Thanks for the preliminary runs. Do you by any chance already have the error.log files?

I can obtain them if you want. Do you need SingleQuery, Incremental, or both?

[martinjonas]

Do you need SingleQuery, Incremental, or both?

Nevermind, I got them both. :-)

Single-query: https://www.fi.muni.cz/~xjonas/smtcomp/processed_results/smtinterpol/smtinterpol.2024-06-12_14-26-36.files.tar.gz
Incremental: https://www.fi.muni.cz/~xjonas/smtcomp/processed_results/smtinterpol_inc/smtinterpol_inc.2024-06-12_14-29-11.files.tar.gz

[jhoenicke]

It looks like the zip file in the archive are all empty. I would suspect that most of the BV benchmarks trigger an output to error.log. And all runs should create at least an empty error.log file. Is this working? Could this be a permission problem, that we can't write to the docker image?

[martinjonas]

It looks like the zip file in the archive are all empty. I would suspect that most of the BV benchmarks trigger an output to error.log. And all runs should create at least an empty error.log file. Is this working? Could this be a permission problem, that we can't write to the docker image?

Ah, it seems that there is some problem of our configuration of cluster for returning the generated files. The file gets created but is not returned from the computation nodes to the server. I will look into that.

[martinjonas]

@jhoenicke We have finished test runs of model-validation and unsat-core generation tracks. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/smtinterpol_model.table.html#/table
• https://www.fi.muni.cz/~xjonas/smtcomp/smtinterpol_unsatcore.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 and only UNSAT for unsat-core generation. 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:

For model-generation: QF_UFFP, QF_UFBVDT, QF_UFDTNIA, QF_NIRA.

For unsat-core: UFBVDT, FPLRA, QF_AUFBVFP, QF_ABVFPLRA, QF_UFBVDT, QF_UFDTNIA, QF_UFDT, QF_NIA, QF_SNIA.

[jhoenicke]

Hi Martin, thanks for the logs. I found two problems:

1. the links to the yml-Files are not working, so it's impossible to see which benchmark it is.
2. it seems that for model-validation, the model is not checked at all. It reports correct for QF_ABV/scrambled63358.smt2, even though the model production crashed.

[martinjonas]

1. the links to the yml-Files are not working, so it's impossible to see which benchmark it is.

Thanks for the report. It should be ok now.

2. it seems that for model-validation, the model is not checked at all. It reports correct for QF_ABV/scrambled63358.smt2, even though the model production crashed.

Yes, this is true. We are just running the solver to check whether it can be executed and not doing any extra post-processing yet. The true in the table corresponds to the result of the (check-sat) result. I see why this can be confusing and it would be better to show ERROR in this case. I will check whether we can do something about that.

[jhoenicke]

I updated the solver binaries for our final submission.