Benchmark Setup

Benchmark CPAchecker MetaVal UAutomizer Witch WitnessLint
Tool CPAchecker 4.0 MetaVal 1.3.1-5-g0b2ff46 UAutomizer 0.3.0-d790fecc Witch 10.0.0-rc1-3aa9cfdd WitnessLint 2.0.3
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
Host apollon* apollon* apollon* apollon* apollon*
OS Linux 6.8.0-51-generic Linux 6.8.0-55-generic Linux 6.8.0-51-generic Linux 6.8.0-51-generic Linux 6.8.0-51-generic
Selected date
Date of execution 2024-12-17 16:39:36 CET 2025-03-11 12:42:10 CET 2024-12-17 16:41:50 CET 2024-12-17 16:43:20 CET 2024-12-17 16:43:52 CET
Run set [cpachecker-validate-violation-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; cpachecker-validate-violation-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [metaval-validate-violation-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; metaval-validate-violation-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [uautomizer-validate-violation-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; uautomizer-validate-violation-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [witch-validate-violation-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; witch-validate-violation-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [witnesslint-validate-violation-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; witnesslint-validate-violation-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow]
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.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

--metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

--full-output --witness-type violation_witness --validate ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

--sv-comp --witness-check ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

--expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 2.0 --witness ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

Statistics

CPAchecker 2024-12-17 16:39:36 CET MetaVal 2025-03-11 12:42:10 CET UAutomizer 2024-12-17 16:41:50 CET Witch 2024-12-17 16:43:20 CET WitnessLint 2024-12-17 16:43:52 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)
all results 103 -639 570 15000 103 0 6.00 840 103 -501 1700 30000 103 159 150 7100 41 0 9.60 810
correct results 51 81 300 8000 0 - - - 62 107 1000 18000 100 159 150 7000 0 - - -
correct true 30 60 170 4600 0 - - - 45 90 690 13000 59 118 83 4100 0 - - -
correct false 21 21 130 3400 0 - - - 17 17 310 5200 41 41 67 2900 0 - - -
correct-unconfirmed results 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
correct-unconfirmed true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
correct-unconfirmed true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
incorrect results 31 -720 190 4900 0 - - - 22 -608 400 7000 0 - - - 0 - - -
incorrect true 14 -448 80 2100 0 - - - 16 -512 250 4800 0 - - - 0 - - -
incorrect false 17 -272 110 2700 0 - - - 6 -96 160 2200 0 - - - 0 - - -

Detailed Results

Background is light blue for void tasks.

CPAchecker 2024-12-17 16:39:36 CET MetaVal 2025-03-11 12:42:10 CET UAutomizer 2024-12-17 16:41:50 CET Witch 2024-12-17 16:43:20 CET WitnessLint 2024-12-17 16:43:52 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)
of 1
showing 0 of 0 tasks