Benchmark Setup
| Benchmark | CPAchecker | MetaVal | UAutomizer | WitnessLint |
|---|---|---|---|---|
| Tool | CPAchecker 4.0 | MetaVal 1.3.1-5-g0b2ff46 | UAutomizer 0.3.0-d790fecc | 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 |
| Host | apollon* | apollon* | apollon* | apollon* |
| OS | [Linux 6.8.0-50-generic; Linux 6.8.0-51-generic] | [Linux 6.8.0-50-generic; Linux 6.8.0-51-generic] | [Linux 6.8.0-50-generic; Linux 6.8.0-51-generic] | [Linux 6.8.0-50-generic; Linux 6.8.0-51-generic] |
| Selected date | ||||
| Date of execution | [2024-12-13 17:38:11 CET; 2024-12-13 17:39:46 CET; 2024-12-13 18:52:53 CET; 2024-12-13 21:08:03 CET; 2024-12-13 21:10:20 CET; 2024-12-14 05:28:47 CET; 2024-12-14 20:29:17 CET; 2024-12-14 20:32:54 CET; 2024-12-14 21:41:45 CET; 2024-12-15 04:23:39 CET; 2024-12-15 04:29:49 CET; 2024-12-16 00:14:54 CET; 2024-12-16 00:15:30 CET; 2024-12-16 00:24:24 CET; 2024-12-16 11:00:08 CET; 2024-12-16 13:50:57 CET; 2024-12-16 15:23:54 CET; 2024-12-16 16:44:02 CET; 2024-12-16 20:43:12 CET; 2024-12-16 23:08:32 CET; 2024-12-17 01:44:10 CET; 2024-12-17 04:03:42 CET] | [2024-12-13 17:40:22 CET; 2024-12-13 18:37:03 CET; 2024-12-13 20:56:41 CET; 2024-12-13 22:12:34 CET; 2024-12-13 22:52:16 CET; 2024-12-14 06:29:39 CET; 2024-12-14 21:04:43 CET; 2024-12-14 21:28:46 CET; 2024-12-15 00:04:31 CET; 2024-12-15 06:48:17 CET; 2024-12-15 09:26:47 CET; 2024-12-16 01:34:48 CET; 2024-12-16 01:46:08 CET; 2024-12-16 03:42:26 CET; 2024-12-16 13:48:28 CET; 2024-12-16 14:05:43 CET; 2024-12-16 17:15:25 CET; 2024-12-16 20:28:33 CET; 2024-12-16 23:25:30 CET; 2024-12-17 00:44:54 CET; 2024-12-17 04:28:11 CET; 2024-12-17 05:29:24 CET] | [2024-12-13 17:40:45 CET; 2024-12-13 18:53:18 CET; 2024-12-13 21:30:11 CET; 2024-12-13 23:52:32 CET; 2024-12-14 00:11:27 CET; 2024-12-14 07:17:54 CET; 2024-12-14 21:55:54 CET; 2024-12-14 22:29:21 CET; 2024-12-15 00:56:54 CET; 2024-12-15 09:50:21 CET; 2024-12-15 14:12:27 CET; 2024-12-16 02:23:42 CET; 2024-12-16 04:11:23 CET; 2024-12-16 08:42:57 CET; 2024-12-16 14:04:39 CET; 2024-12-16 14:13:56 CET; 2024-12-16 20:46:27 CET; 2024-12-16 22:44:03 CET; 2024-12-17 01:02:27 CET; 2024-12-17 01:43:19 CET; 2024-12-17 05:09:07 CET; 2024-12-17 08:26:55 CET] | [2024-12-13 17:50:04 CET; 2024-12-13 19:37:57 CET; 2024-12-13 21:49:02 CET; 2024-12-14 00:24:42 CET; 2024-12-14 01:38:33 CET; 2024-12-14 12:32:28 CET; 2024-12-14 22:14:28 CET; 2024-12-14 22:59:45 CET; 2024-12-15 01:26:06 CET; 2024-12-15 13:55:24 CET; 2024-12-15 18:18:15 CET; 2024-12-16 05:05:01 CET; 2024-12-16 08:09:17 CET; 2024-12-16 10:58:01 CET; 2024-12-16 14:18:22 CET; 2024-12-16 14:38:17 CET; 2024-12-16 21:53:07 CET; 2024-12-16 23:20:00 CET; 2024-12-17 01:24:48 CET; 2024-12-17 03:14:03 CET; 2024-12-17 07:55:49 CET; 2024-12-17 10:52:54 CET] |
| Run set | [cpachecker-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-BitVectors; cpachecker-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainControlFlow; cpachecker-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainHeap; cpachecker-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-Other] | [metaval-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-BitVectors; metaval-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainControlFlow; metaval-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainHeap; metaval-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-Other] | [uautomizer-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-BitVectors; uautomizer-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainControlFlow; uautomizer-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainHeap; uautomizer-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-Other] | [witnesslint-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-BitVectors; witnesslint-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainControlFlow; witnesslint-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-MainHeap; witnesslint-validate-violation-witnesses-v1.SV-COMP25_termination.Termination-Other] |
| 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/2ls.2024-11-29_11-00-37.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/aprove.2024-11-29_11-05-40.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/bubaak-split.2024-11-29_23-04-32.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/bubaak.2024-11-29_13-23-21.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/cbmc.2024-12-09_14-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/cpachecker.2024-11-30_06-09-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/divine.2024-12-10_08-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/emergentheta.2024-12-01_23-22-13.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/esbmc-kind.2024-12-02_10-54-34.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/goblint.2024-11-29_20-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/graves.2024-12-10_14-44-07.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/mopsa.2024-12-02_20-14-42.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/nacpa.2024-12-03_05-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/pesco.2024-12-13_11-12-50.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/pinaka.2024-12-12_03-17-29.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/proton.2024-11-29_11-06-15.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/symbiotic.2024-12-01_13-17-06.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/theta.2024-12-03_22-56-58.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/thorn.2024-12-04_10-40-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/uautomizer.2024-11-30_15-04-55.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/ukojak.2024-12-05_21-20-14.files/${rundefinition_name}/${taskdef_name}/witness.graphml --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/utaipan.2024-12-05_21-21-41.files/${rundefinition_name}/${taskdef_name}/witness.graphml |
--metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/2ls.2024-11-29_11-00-37.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/aprove.2024-11-29_11-05-40.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/bubaak-split.2024-11-29_23-04-32.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/bubaak.2024-11-29_13-23-21.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/cbmc.2024-12-09_14-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/cpachecker.2024-11-30_06-09-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/divine.2024-12-10_08-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/emergentheta.2024-12-01_23-22-13.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/esbmc-kind.2024-12-02_10-54-34.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/goblint.2024-11-29_20-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/graves.2024-12-10_14-44-07.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/mopsa.2024-12-02_20-14-42.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/nacpa.2024-12-03_05-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/pesco.2024-12-13_11-12-50.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/pinaka.2024-12-12_03-17-29.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/proton.2024-11-29_11-06-15.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/symbiotic.2024-12-01_13-17-06.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/theta.2024-12-03_22-56-58.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/thorn.2024-12-04_10-40-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/uautomizer.2024-11-30_15-04-55.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/ukojak.2024-12-05_21-20-14.files/${rundefinition_name}/${taskdef_name}/witness.graphml --metavalWitnessType violation_witness --metavalVerifierBackend cpachecker --predicateAnalysis --heap 5000M --benchmark --timelimit 90s --metavalWitness ../../results-verified/utaipan.2024-12-05_21-21-41.files/${rundefinition_name}/${taskdef_name}/witness.graphml |
--full-output --witness-type violation_witness --validate ../../results-verified/2ls.2024-11-29_11-00-37.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/aprove.2024-11-29_11-05-40.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/bubaak-split.2024-11-29_23-04-32.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/bubaak.2024-11-29_13-23-21.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/cbmc.2024-12-09_14-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/cpachecker.2024-11-30_06-09-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/divine.2024-12-10_08-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/emergentheta.2024-12-01_23-22-13.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/esbmc-kind.2024-12-02_10-54-34.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/goblint.2024-11-29_20-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/graves.2024-12-10_14-44-07.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/mopsa.2024-12-02_20-14-42.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/nacpa.2024-12-03_05-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/pesco.2024-12-13_11-12-50.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/pinaka.2024-12-12_03-17-29.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/proton.2024-11-29_11-06-15.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/symbiotic.2024-12-01_13-17-06.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/theta.2024-12-03_22-56-58.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/thorn.2024-12-04_10-40-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/uautomizer.2024-11-30_15-04-55.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/ukojak.2024-12-05_21-20-14.files/${rundefinition_name}/${taskdef_name}/witness.graphml --full-output --witness-type violation_witness --validate ../../results-verified/utaipan.2024-12-05_21-21-41.files/${rundefinition_name}/${taskdef_name}/witness.graphml |
--expectViolationWitness --ignoreSelfLoops --excludeRecentChecks 0 --expectedWitnessVersion 1.0 --witness ../../results-verified/cbmc.2024-12-09_14-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --excludeRecentChecks 0 --expectedWitnessVersion 1.0 --witness ../../results-verified/divine.2024-12-10_08-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --excludeRecentChecks 0 --expectedWitnessVersion 1.0 --witness ../../results-verified/graves.2024-12-10_14-44-07.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --excludeRecentChecks 0 --expectedWitnessVersion 1.0 --witness ../../results-verified/pesco.2024-12-13_11-12-50.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --excludeRecentChecks 0 --expectedWitnessVersion 1.0 --witness ../../results-verified/pinaka.2024-12-12_03-17-29.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/2ls.2024-11-29_11-00-37.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/aprove.2024-11-29_11-05-40.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/bubaak-split.2024-11-29_23-04-32.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/bubaak.2024-11-29_13-23-21.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/cpachecker.2024-11-30_06-09-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/emergentheta.2024-12-01_23-22-13.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/esbmc-kind.2024-12-02_10-54-34.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/goblint.2024-11-29_20-22-51.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/mopsa.2024-12-02_20-14-42.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/nacpa.2024-12-03_05-22-17.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/proton.2024-11-29_11-06-15.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/symbiotic.2024-12-01_13-17-06.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/theta.2024-12-03_22-56-58.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/thorn.2024-12-04_10-40-11.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/uautomizer.2024-11-30_15-04-55.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/ukojak.2024-12-05_21-20-14.files/${rundefinition_name}/${taskdef_name}/witness.graphml --expectViolationWitness --ignoreSelfLoops --expectedWitnessVersion 1.0 --witness ../../results-verified/utaipan.2024-12-05_21-21-41.files/${rundefinition_name}/${taskdef_name}/witness.graphml |
Statistics
| CPAchecker 2024-12-17 04:03:42 CET | MetaVal 2024-12-17 05:29:24 CET | UAutomizer 2024-12-17 08:26:55 CET | WitnessLint 2024-12-17 10:52:54 CET | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| all results | 6433 | 2058 | 190000 | 1700000 | 6433 | 0 | 5100 | 330000 | 6433 | 2058 | 170000 | 3300000 | 17524 | 0 | 3600 | 360000 |
| correct results | 2057 | 2058 | 34000 | 440000 | 0 | - | - | - | 2057 | 2058 | 59000 | 1000000 | 0 | - | - | - |
| correct true | 1 | 2 | 8.00 | 170 | 0 | - | - | - | 1 | 2 | 27 | 530 | 0 | - | - | - |
| correct false | 2056 | 2056 | 34000 | 440000 | 0 | - | - | - | 2056 | 2056 | 59000 | 1000000 | 0 | - | - | - |
| correct-unconfirmed results | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - |
| correct-unconfirmed true | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - |
| correct-unconfirmed true | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - |
| incorrect results | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - |
| incorrect true | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - |
| incorrect false | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - | 0 | - | - | - |
Detailed Results
Background is light blue for void tasks.
| CPAchecker 2024-12-17 04:03:42 CET | MetaVal 2024-12-17 05:29:24 CET | UAutomizer 2024-12-17 08:26:55 CET | WitnessLint 2024-12-17 10:52:54 CET | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|