Benchmark Setup

Benchmark CPAchecker MetaVal Theta UAutomizer Witch WitnessLint
Tool CPAchecker 4.2.2 MetaVal 2.0.0-dev Theta 6.27.9 UAutomizer 0.3.1-35a84365 Witch 4.0.0-rc1-ffc643de WitnessLint 2.1.2
Limits timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host 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
Selected date
Date of execution 2026-01-01 08:12:08 CET 2026-01-01 08:17:15 CET 2026-01-01 08:19:21 CET 2026-01-01 08:22:38 CET 2026-01-01 08:23:42 CET 2026-01-01 08:24:48 CET
Run set [cpachecker-validate-violation-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; cpachecker-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; cpachecker-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [metaval-validate-violation-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; metaval-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; metaval-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [theta-validate-violation-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; theta-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; theta-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [uautomizer-validate-violation-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; uautomizer-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; uautomizer-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [witch-validate-violation-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; witch-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; witch-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses] [witnesslint-validate-violation-witnesses-v2.SV-COMP26_C.termination.ViolationWitnesses; witnesslint-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.CorrectnessWitnesses; witnesslint-validate-violation-witnesses-v2.SV-COMP26_C.unreach-call.ViolationWitnesses]
Options

--violation-witness-validation --heap 5000m --benchmark --option witness.checkProgramHash=false --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --option cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc --option cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc --option cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc --option cpa.smg.deallocationFunctions=free,kfree,kfree_const --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 violation --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 violation_witness --validate ../../results-verified/witnessmap.2026-01-01_08-06-12.files/${rundefinition_name}/${taskdef_name}/witness.yml

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

--expectViolationWitness --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:08 CET MetaVal 2026-01-01 08:17:15 CET Theta 2026-01-01 08:19:21 CET UAutomizer 2026-01-01 08:22:38 CET Witch 2026-01-01 08:23:42 CET WitnessLint 2026-01-01 08:24:48 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)
all results 135 24 810 19000 135 -658 1200 28000 135 7 3700 40000 135 -548 2200 39000 135 181 340 7600 53 0 13 1500
correct results 57 88 410 9300 39 46 450 11000 5 7 48 910 65 108 1100 21000 115 181 150 7100 0 - - -
correct true 31 62 230 5100 7 14 75 1900 2 4 19 340 43 86 680 14000 66 132 79 4100 0 - - -
correct false 26 26 180 4300 32 32 370 9300 3 3 28 570 22 22 390 7400 49 49 68 3000 0 - - -
correct-unconfirmed results 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
correct-unconfirmed true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
correct-unconfirmed true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
incorrect results 4 -64 110 940 41 -704 520 12000 0 - - - 26 -656 490 8800 0 - - - 0 - - -
incorrect true 0 - - - 3 -96 33 810 0 - - - 15 -480 240 4800 0 - - - 0 - - -
incorrect false 4 -64 110 940 38 -608 490 11000 0 - - - 11 -176 250 4000 0 - - - 0 - - -

Detailed Results

Background is light blue for void tasks.

CPAchecker 2026-01-01 08:12:08 CET MetaVal 2026-01-01 08:17:15 CET Theta 2026-01-01 08:19:21 CET UAutomizer 2026-01-01 08:22:38 CET Witch 2026-01-01 08:23:42 CET WitnessLint 2026-01-01 08:24:48 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)
of 1
showing 0 of 0 tasks