SMTS submission 2025

[Tomaqa]

No description provided.

[github-actions]

Summary of modified submissions

SMTS

• 3 authors
• website: https://github.com/usi-verification-and-security/SMTS
• Participations
  • Parallel
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • QF_UFDTLIA
      • QF_UFDTLIRA
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all

[martinjonas]

@Tomaqa Thanks for submitting SMTS to SMT-COMP 2025! We have tried running test runs and we ran into few technical problems.

1. The path to the executable in the command field has to be relative to the directory where the archive was unpacked and the arguments should be separate items in the list. Ideally also do not call python3 executable, but directly your solver's entry point. And there is no variable <path>. When I changed the command in your submission from

   "command": ["python3 ./server/smts.py -l -p -o 256", "-fp <path>"],
   

   to

   "command": ["./SMTS/server/smts.py", "-l", "-p", "-o 256", "-fp"],
   

   I was able to execute your solver on our infrastructure. Can you make such a change in your submission? Thanks!

2. We do not have git installed on the worker machines in our cluster. So the import from version import version in server/smts.py fails because it calls version.sh, which calls git, which fails. Can you remove the dependency on git? We are not administrators of the cluster and cannot install git to all of the machines.

3. When I fixed that, I was able to execute the solver and get the results. You can find the results here: https://www.fi.muni.cz/~xjonas/smtcomp/tables/smts_parallel.table.html#/table

   Unfortunately, the solver currently does not produce the output in SMT-LIB compliant format. For example, on the benchmark QF_UFIDL/QF_UFIDL_20210312-Bouvier_vlsat3_f10.smt2 , the output is

   /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_94a9aa27-0d02-4702-8db4-c6e781b870d1/unpack/1f46314b1d932a7a15eb21c43350fa85a0a85f4ad82c5d522615a4c528eb8da5/SMTS/server/utils.py:184: SyntaxWarning: invalid escape sequence '\{'
     s = re.sub('(\{[0-9]*\})', lambda x: strings[x.group(1)], s)
   scrambled16421.smt2 unsat 24.13
   

   instead of just

   unsat
   

We are going to announce a deadline extension until the end of Sunday (GMT) soon. If you update the submission by then, I can rerun the test runs.

[Tomaqa]

I hope I fixed all your comments. Thank you for re-running the tests!

[martinjonas]

@Tomaqa Thanks a lot for all of the changes! Good news is that it solves almost all of the problems. The execution still does not work, but if you split all the command line arguments, the execution goes through (we have to document the JSON better next year and also provide CI for the Parallel track). I.e., please change

"command": ["./SMTS/server/smts.py", "-l", "-p", "-pt 2", "-o 256", "-fp"],

to

"command": ["./SMTS/server/smts.py", "-l", "-p", "-pt", "2", "-o", "256", "-fp"],

I have done that and ran the test runs. The results are here: https://www.fi.muni.cz/~xjonas/smtcomp/tables/smts_parallel.table.html#/table

The worse news is that the solver returns 4 incorrect results, i.e., returns unsat (false) on benchmarks with expected status sat (true). You can find the benchmarks in the table marked by the status in red font.

For the investigation, you can find the scrambled benchmarks here: https://www.fi.muni.cz/~xjonas/smtcomp/benchmarks/parallel.tar.gz . The archive contains for each original benchmark a file ORIGINAL_NAME.yml, in which you can find the name of the scrambled benchmark.

If you think that there is an issue on our side, please let me know.

[Tomaqa]

Thank you for the update. I indeed reproduced one of the bugs and observed that it works properly when using just 64 solvers. We will need to investigate - after the competition.
I updated the submission accordingly. Could you please run the tests once again? I hope it will be fine now.
Thanks.

[martinjonas]

Thanks for the update, you can find the new results on the same link as before. The execution is working fine now. Unfortunately, there are still two incorrect answers remaining. :/

Again, if you think that the problem is on our side or the benchmark has wrong expected result, let me know. Also let me know if you want another test run with a fixed version. We still have some time left and the test executions are quite quick.

[Tomaqa]

I tried the above link (https://www.fi.muni.cz/~xjonas/smtcomp/tables/smts_parallel.table.html#/table) but even though it shows the date 06-28, there are more incorrect results than two, and the one that I supposedly fixed does not seem to be fixed (QF_LRA_miplib_danoint-66). Are the results at that link up-to-date or not?
If not, can you tell me on which two instances it failed?

[martinjonas]

Sorry for the confusion, I must have uploaded some inconsistent mix of two result sets. To be sure, I ran the tests again and updated the results. There is still one incorrect result in the latest run.

[Tomaqa]

I hope I found the culprit. Even if not, let's use this anyway.