Benchmark Setup

Benchmark CPAchecker Goblint LIV MetaVal Mopsa Theta UAutomizer UReferee WitnessLint
Tool CPAchecker 4.2.2 Goblint tags/svcomp26-0-gbb55b70d9 LIV 2.0.0-dev MetaVal 2.0.0-dev Mopsa 1.2 (git branch:feature/sv-comp commit:301819dd0 commit-date:2025-11-23 23:39:36 +0100) Theta 6.27.9 UAutomizer 0.3.1-00d43373 UReferee 0.3.1-00d43373 WitnessLint 2.1.2
Limits timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 300 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* apollon* apollon* apollon* apollon* apollon* apollon* apollon* apollon*
OS Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic Linux 6.8.0-88-generic
Selected date
Date of execution 2026-01-01 08:12:07 CET 2026-01-01 08:12:02 CET 2026-01-01 08:12:44 CET 2026-01-01 08:16:14 CET 2026-01-01 08:17:13 CET 2026-01-01 08:18:08 CET 2026-01-01 08:21:15 CET 2026-01-01 08:23:11 CET 2026-01-01 08:24:32 CET
Run set [cpachecker-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; cpachecker-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; cpachecker-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [goblint-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; goblint-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; goblint-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [liv-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; liv-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; liv-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [metaval-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; metaval-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; metaval-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [mopsa-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; mopsa-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; mopsa-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [theta-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; theta-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; theta-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [uautomizer-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; uautomizer-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; uautomizer-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [ureferee-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; ureferee-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; ureferee-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [witnesslint-validate-correctness-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; witnesslint-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; witnesslint-validate-correctness-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses]
Options

--correctness-witness-validation --heap 5000m --benchmark --option witness.checkProgramHash=false --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --witness ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--portfolio-conf conf/svcomp26/seq-validate.txt --witness.yaml.unassume ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--config ./config/liv-runexec.yml --witness ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--config ./config/svcomp26.yml --debug --expect-witness-type correctness --witness ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--validate_yaml_witness ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--svcomp --portfolio STABLE --loglevel RESULT --witness ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--full-output --witness-type correctness_witness --validate ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--full-output --witness-type correctness_witness --validate ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

--expectCorrectnessWitness --ignoreSelfLoops --expectedWitnessVersion 2 --witness ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

Statistics

CPAchecker 2026-01-01 08:12:07 CET Goblint 2026-01-01 08:12:02 CET LIV 2026-01-01 08:12:44 CET MetaVal 2026-01-01 08:16:14 CET Mopsa 2026-01-01 08:17:13 CET Theta 2026-01-01 08:18:08 CET UAutomizer 2026-01-01 08:21:15 CET UReferee 2026-01-01 08:23:11 CET WitnessLint 2026-01-01 08:24:32 CET
Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB) Amount Raw score CPU (s) Mem (MB)
all results 135 18 1200 15000 135 22 20000 44000 135 -64 450 5900 135 14 670 11000 135 24 7200 16000 135 7 13000 42000 135 14 820 7300 135 12 460 6700 82 0 21 2300
correct results 9 18 86 1600 11 22 2.90 340 0 - - - 16 30 250 5100 12 24 28 960 5 7 47 910 16 30 440 5600 6 12 94 1900 0 - - -
correct true 9 18 86 1600 11 22 2.90 340 0 - - - 14 28 230 4500 12 24 28 960 2 4 19 350 14 28 400 4900 6 12 94 1900 0 - - -
correct false 0 - - - 0 - - - 0 - - - 2 2 21 570 0 - - - 3 3 28 560 2 2 36 650 0 - - - 0 - - -
correct-unconfirmed results 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
correct-unconfirmed true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
correct-unconfirmed true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
incorrect results 0 - - - 0 - - - 4 -64 200 1100 1 -16 9.80 290 0 - - - 0 - - - 1 -16 16 320 0 - - - 0 - - -
incorrect true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
incorrect false 0 - - - 0 - - - 4 -64 200 1100 1 -16 9.80 290 0 - - - 0 - - - 1 -16 16 320 0 - - - 0 - - -

Detailed Results

Background is light blue for void tasks.

CPAchecker 2026-01-01 08:12:07 CET Goblint 2026-01-01 08:12:02 CET LIV 2026-01-01 08:12:44 CET MetaVal 2026-01-01 08:16:14 CET Mopsa 2026-01-01 08:17:13 CET Theta 2026-01-01 08:18:08 CET UAutomizer 2026-01-01 08:21:15 CET UReferee 2026-01-01 08:23:11 CET WitnessLint 2026-01-01 08:24:32 CET
Benchmark | Property | Expected result | Witness category | Run set Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB) Status Raw score CPU (s) Mem (MB)
of 1
showing 0 of 0 tasks