diff --git a/submissions/bitwuzla.json b/submissions/bitwuzla.json index 43d6f6ed..8982e20d 100644 --- a/submissions/bitwuzla.json +++ b/submissions/bitwuzla.json @@ -39,7 +39,7 @@ { "tracks": ["Parallel"], "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", - "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "128"] + "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "64"] } ] } diff --git a/submissions/bitwuzla_parallel_16.json b/submissions/bitwuzla_parallel_16.json new file mode 100644 index 00000000..02a0abdb --- /dev/null +++ b/submissions/bitwuzla_parallel_16.json @@ -0,0 +1,27 @@ +{ + "name": "Bitwuzla", + "contributors": ["Aina Niemetz", "Mathias Preiner"], + "contacts": ["Mathias Preiner "], + "final" : true, + + "archive": { + "url": "https://zenodo.org/records/15760031/files/bitwuzla-submission-smtcomp-2025.zip?download=1", + "h": {"sha256": "b97f018f4d92978c6b116c3f0b09f44f06ec15c885f6cc84a9dde3218cc1a583"} + }, + + "command": ["bin/bitwuzla"], + + "website": "https://bitwuzla.github.io", + "system_description": "https://bitwuzla.github.io/data/smtcomp2025/paper.pdf", + "solver_type": "Standalone", + "seed": "42", + "competitive": false, + "participations": [ + { + "tracks": ["Parallel"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "16"] + } + ] +} + diff --git a/submissions/bitwuzla_parallel_32.json b/submissions/bitwuzla_parallel_32.json new file mode 100644 index 00000000..06113d44 --- /dev/null +++ b/submissions/bitwuzla_parallel_32.json @@ -0,0 +1,27 @@ +{ + "name": "Bitwuzla", + "contributors": ["Aina Niemetz", "Mathias Preiner"], + "contacts": ["Mathias Preiner "], + "final" : true, + + "archive": { + "url": "https://zenodo.org/records/15760031/files/bitwuzla-submission-smtcomp-2025.zip?download=1", + "h": {"sha256": "b97f018f4d92978c6b116c3f0b09f44f06ec15c885f6cc84a9dde3218cc1a583"} + }, + + "command": ["bin/bitwuzla"], + + "website": "https://bitwuzla.github.io", + "system_description": "https://bitwuzla.github.io/data/smtcomp2025/paper.pdf", + "solver_type": "Standalone", + "seed": "42", + "competitive": false, + "participations": [ + { + "tracks": ["Parallel"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "32"] + } + ] +} +