Benchmark Setup

Benchmark CPAchecker Goblint LIV MetaVal MetaVal++ Mopsa UAutomizer UReferee WitnessLint
Tool CPAchecker 4.0 Goblint tags/svcomp25-0-g5512d834b LIV 0.2-dev MetaVal 1.3.1-5-g0b2ff46 MetaVal++ 0.0.1-dev Mopsa 1.0 (git branch:feature/sv-comp commit:295e3e262 commit-date:2024-11-23 10:10:19 +0100) UAutomizer 0.3.0-d790fecc UReferee 0.3.0-d790fecc WitnessLint 2.0.3
Limits timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* apollon* apollon* apollon* apollon* apollon* apollon* apollon* apollon*
OS Linux 6.8.0-51-generic Linux 6.8.0-51-generic 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 Linux 6.8.0-51-generic Linux 6.8.0-51-generic
Selected date
Date of execution 2024-12-17 16:39:36 CET 2024-12-17 16:39:31 CET 2024-12-17 16:40:01 CET 2025-03-11 12:42:10 CET 2024-12-17 16:41:00 CET 2024-12-17 16:41:23 CET 2024-12-17 16:41:43 CET 2024-12-17 16:43:08 CET 2024-12-17 16:43:24 CET
Run set [cpachecker-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; cpachecker-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [goblint-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; goblint-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [liv-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; liv-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [metaval-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; metaval-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [metaval++-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; metaval++-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [mopsa-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; mopsa-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [uautomizer-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; uautomizer-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [ureferee-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; ureferee-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow] [witnesslint-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.CorrectnessWitnesses-Loops; witnesslint-validate-correctness-witnesses-v2.SV-COMP25_unreach-call.ViolationWitnesses-ControlFlow]
Options

--correctness-witness-validation --heap 5000m --benchmark --option witness.checkProgramHash=false --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --witness ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

--conf conf/svcomp25-validate.json --witness.yaml.unassume ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

--verifier actors/cbmc.yml --verifierversion default --cache-dir lib/cvt_cache --no-cache-update --all-possible-invariant-locations --fuzzy-invariant-locations 1 --non-strict --prep-cgroup --debug --witness ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

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

--backend framac-wp --debug --witness ../../results-verified/witnessmap.2024-11-29_14-08-33.files/${rundefinition_name}/${taskdef_name}/witness.yml

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

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

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

--expectCorrectnessWitness --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 Goblint 2024-12-17 16:39:31 CET LIV 2024-12-17 16:40:01 CET MetaVal 2025-03-11 12:42:10 CET MetaVal++ 2024-12-17 16:41:00 CET Mopsa 2024-12-17 16:41:23 CET UAutomizer 2024-12-17 16:41:43 CET UReferee 2024-12-17 16:43:08 CET WitnessLint 2024-12-17 16:43:24 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 6 6 3300 7500 6 0 0.78 140 6 0 260 400 6 0 0.33 49 6 0 180 5100 6 0 630 830 6 6 230 2100 6 0 180 1700 3 0 0.67 59
correct results 3 6 560 630 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 3 6 150 1200 0 - - - 0 - - -
correct true 3 6 560 630 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 3 6 150 1200 0 - - - 0 - - -
correct false 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 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 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
incorrect true 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
incorrect false 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -

Detailed Results

Background is light blue for void tasks.

CPAchecker 2024-12-17 16:39:36 CET Goblint 2024-12-17 16:39:31 CET LIV 2024-12-17 16:40:01 CET MetaVal 2025-03-11 12:42:10 CET MetaVal++ 2024-12-17 16:41:00 CET Mopsa 2024-12-17 16:41:23 CET UAutomizer 2024-12-17 16:41:43 CET UReferee 2024-12-17 16:43:08 CET WitnessLint 2024-12-17 16:43:24 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