search

ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

Adding smoke test to xcfa-cli #241

Closed leventeBajczi closed 1 year ago

leventeBajczi commented 1 year ago

Benchexec is run against all common targets in SV-COMP, and a summary is printed as a comment on PRs.

sonarcloud[bot] commented 1 year ago

Kudos, SonarCloud Quality Gate passed!    Quality Gate passed

Bug A 0 Bugs
Vulnerability A 0 Vulnerabilities
Security Hotspot A 0 Security Hotspots
Code Smell A 0 Code Smells

No Coverage information No Coverage information
No Duplication information No Duplication information

github-actions[bot] commented 1 year ago

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

:question: ConcurrencySafety-Main (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ConcurrencySafety-Main/theta.2023-11-12_17-50-43.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ConcurrencySafety-Main/theta.2023-11-12_17-50-43.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ConcurrencySafety-Main, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:50:43 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1456-892 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.787 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ConcurrencySafety-Main Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------- pthread-atomic/read_write_lock-1.yml ERROR (server error) 3.94 1.42 None pthread-wmm/rfi003_tso.yml ERROR (server error) 4.51 1.61 None pthread/lazy01.yml ERROR (server error) 3.84 1.43 None pthread-wmm/mix000.oepc.yml ERROR (server error) 4.37 1.57 None pthread-wmm/safe032_tso.yml ERROR (server error) 3.36 1.26 None pthread-wmm/safe030_tso.yml ERROR (server error) 4.19 1.53 None pthread-wmm/safe018_power.opt.yml ERROR (server error) 4.38 1.57 None pthread-wmm/safe026_tso.yml ERROR (server error) 3.91 1.44 None pthread/fib_safe-11.yml ERROR (server error) 4.02 1.44 None pthread-wmm/safe024_tso.yml ERROR (server error) 4.34 1.59 None ----------------------------------------------------------------------------------------------------- Run set 1 done 40.86 15.90 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 17) ```
:question: ConcurrencySafety-MemSafety (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ConcurrencySafety-MemSafety/theta.2023-11-12_17-50-36.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ConcurrencySafety-MemSafety/theta.2023-11-12_17-50-36.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety date: Sun, 2023-11-12 17:50:36 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1535-641 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3270.617 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety Run set 4 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------- pthread-atomic/read_write_lock-1.yml ERROR (server error) 4.11 1.53 None pthread-wmm/rfi003_tso.yml ERROR (server error) 3.78 1.36 None pthread/lazy01.yml ERROR (server error) 3.89 1.45 None pthread-wmm/mix000.oepc.yml ERROR (server error) 4.40 1.58 None pthread-wmm/safe032_tso.yml ERROR (server error) 3.33 1.23 None pthread-wmm/safe030_tso.yml ERROR (server error) 4.13 1.51 None pthread-wmm/safe018_power.opt.yml ERROR (server error) 4.46 1.61 None pthread-wmm/safe026_tso.yml ERROR (server error) 4.06 1.50 None pthread/fib_safe-11.yml ERROR (server error) 4.14 1.52 None pthread-wmm/safe024_tso.yml ERROR (server error) 4.19 1.54 None ----------------------------------------------------------------------------------------------------- Run set 4 done 40.48 15.86 - Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 20) ```
:question: ConcurrencySafety-NoOverflows (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2023-11-12_17-50-34.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2023-11-12_17-50-34.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:50:34 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az773-392 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3241.35 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows Run set 3 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------- pthread-atomic/read_write_lock-1.yml ERROR (server error) 3.74 1.38 None pthread-wmm/rfi003_tso.yml ERROR (server error) 3.80 1.35 None pthread/lazy01.yml ERROR (server error) 3.75 1.40 None pthread-wmm/mix000.oepc.yml ERROR (server error) 4.32 1.55 None pthread-wmm/safe032_tso.yml ERROR (server error) 3.45 1.30 None pthread-wmm/safe030_tso.yml ERROR (server error) 4.07 1.49 None pthread-wmm/safe018_power.opt.yml ERROR (server error) 4.51 1.60 None pthread-wmm/safe026_tso.yml ERROR (server error) 3.46 1.28 None pthread/fib_safe-11.yml ERROR (server error) 3.74 1.37 None pthread-wmm/safe024_tso.yml ERROR (server error) 3.47 1.30 None ----------------------------------------------------------------------------------------------------- Run set 3 done 38.31 15.06 - SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 20) ```
:question: NoDataRace-Main (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-NoDataRace-Main/theta.2023-11-12_17-51-55.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-NoDataRace-Main/theta.2023-11-12_17-51-55.results.SV-COMP24_no-data-race.NoDataRace-Main.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race.NoDataRace-Main, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:51:55 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az470-368 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: Intel Xeon Platinum 8171M CPU @ 2.60GHz - cores: 2 - max frequency: 2095.078 MHz ram: 7258.226688 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race.NoDataRace-Main Run set 2 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------- pthread-atomic/read_write_lock-1.yml ERROR (server error) 3.43 2.00 None pthread-wmm/rfi003_tso.yml ERROR (server error) 3.65 2.09 None pthread/lazy01.yml ERROR (server error) 3.24 1.89 None pthread-wmm/mix000.oepc.yml ERROR (server error) 3.36 1.88 None pthread-wmm/safe032_tso.yml ERROR (server error) 3.43 1.91 None pthread-wmm/safe030_tso.yml ERROR (server error) 3.48 1.96 None pthread-wmm/safe018_power.opt.yml ERROR (server error) 3.43 1.90 None pthread-wmm/safe026_tso.yml ERROR (server error) 3.24 1.80 None pthread/fib_safe-11.yml ERROR (server error) 3.04 1.72 None pthread-wmm/safe024_tso.yml ERROR (server error) 3.45 1.94 None ----------------------------------------------------------------------------------------------------- Run set 2 done 33.79 20.15 - SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 20) ```
:question: ReachSafety-Arrays (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Arrays/theta.2023-11-12_17-49-44.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Arrays/theta.2023-11-12_17-49-44.results.SV-COMP24_unreach-call.ReachSafety-Arrays.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Arrays, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:49:44 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az180-373 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: Intel Xeon Platinum 8272CL CPU @ 2.60GHz - cores: 2 - max frequency: 2593.907 MHz ram: 7258.222592 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Arrays Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------------------------------- array-examples/standard_partition_ground-2.yml TIMEOUT 120.41 113.90 None array-programs/copysome2-1.yml TIMEOUT 120.46 113.51 None array-examples/sanfoundry_24-1.yml TIMEOUT 120.60 109.25 None array-multidimensional/max-2-u.yml ERROR (server error) 1.96 1.17 None array-examples/sorting_bubblesort_ground-1.yml TIMEOUT 120.37 113.70 None array-multidimensional/rev-2-n-u.yml ERROR (server error) 2.01 1.18 None array-examples/data_structures_set_multi_proc_trivial_ground.yml TIMEOUT 120.35 114.03 None array-patterns/array21_pattern.yml ERROR (server error) 1.98 1.19 None array-examples/standard_copy3_ground-2.yml TIMEOUT 120.36 113.81 None array-examples/standard_copy6_ground-2.yml TIMEOUT 120.38 113.13 None --------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 6.91 798.66 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 19) ```
:white_check_mark: ReachSafety-BitVectors (6 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-BitVectors/theta.2023-11-12_17-48-09.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-BitVectors/theta.2023-11-12_17-48-09.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-BitVectors, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:48:09 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1200-393 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3228.633 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-BitVectors Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------ bitvector/gcd_4.yml true 2.84 1.07 None bitvector/soft_float_1-3a.c.cil.yml ERROR (server error) 3.15 1.19 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 2.74 1.08 None bitvector/sum02-1.yml TIMEOUT 120.56 112.68 None bitvector-loops/diamond_2-1.yml TIMEOUT 120.54 112.21 None bitvector-regression/signextension-1.yml false(unreach-call) 2.72 1.04 None bitvector/s3_srvr_3a.BV.c.cil.yml TIMEOUT 120.73 108.86 None bitvector-regression/signextension2-2.yml false(unreach-call) 2.82 1.10 None bitvector/s3_clnt_2.BV.c.cil-1a.yml true 8.94 3.03 None bitvector/s3_srvr_2a.BV.c.cil.yml true 9.39 3.64 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 32.96 347.24 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 6 correct true: 3 correct false: 3 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 9 (max: 14) ```
:question: ReachSafety-Combinations (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Combinations/theta.2023-11-12_17-49-48.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Combinations/theta.2023-11-12_17-49-48.results.SV-COMP24_unreach-call.ReachSafety-Combinations.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Combinations, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:49:48 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1435-737 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2839.237 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Combinations Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------------------------- pc_sfifo_3.cil+token_ring.02.cil-2.yml TIMEOUT 120.84 99.48 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.82 82.77 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 120.56 100.23 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.93 82.59 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 121.14 90.16 None pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 120.05 100.01 None pals_lcr.4_overflow.ufo.UNBOUNDED.pals+Problem12_label09.yml TIMEOUT 121.01 90.17 None pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label09.yml TIMEOUT 120.25 98.46 None Problem05_label42+token_ring.05.cil-1.yml TIMEOUT 120.95 83.90 None Problem05_label42+token_ring.07.cil-1.yml TIMEOUT 120.50 83.15 None ----------------------------------------------------------------------------------------------------------------------------- Run set 1 done 1.23 913.47 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 13) ```
:white_check_mark: ReachSafety-ControlFlow (7 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-ControlFlow/theta.2023-11-12_17-48-12.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-ControlFlow/theta.2023-11-12_17-48-12.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-ControlFlow, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:48:12 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1383-850 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3086.69 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ControlFlow Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------ locks/test_locks_11.yml true 38.07 29.03 None locks/test_locks_5.yml true 4.01 1.37 None locks/test_locks_9.yml true 12.10 4.93 None locks/test_locks_14-2.yml false(unreach-call) 4.42 1.53 None locks/test_locks_6.yml true 4.90 1.72 None locks/test_locks_12.yml TIMEOUT 120.86 109.23 None unsignedintegeroverflow-sas23/cancel_var_through_overflow.yml TIMEOUT 120.17 118.49 None locks/test_locks_8.yml true 8.85 3.04 None unsignedintegeroverflow-sas23/linear_interpolation_2.yml ERROR (server error) 10.20 8.56 None locks/test_locks_7.yml true 5.97 2.05 None ------------------------------------------------------------------------------------------------------------------------------ Run set 1 done 88.76 281.18 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 7 correct true: 6 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 3 Score: 13 (max: 19) ```
:question: ReachSafety-ECA (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-ECA/theta.2023-11-12_17-51-23.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-ECA/theta.2023-11-12_17-51-23.results.SV-COMP24_unreach-call.ReachSafety-ECA.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-ECA, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:51:23 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1383-850 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2946.048 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ECA Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------- eca-rers2012/Problem06_label18.yml TIMEOUT 120.67 94.22 None eca-rers2012/Problem06_label11.yml TIMEOUT 120.37 92.83 None eca-programs/Problem101_label07.yml TIMEOUT 121.62 70.07 None eca-rers2012/Problem05_label44.yml TIMEOUT 120.42 91.82 None eca-rers2012/Problem04_label05.yml TIMEOUT 121.02 99.74 None eca-rers2012/Problem18_label36.yml TIMEOUT 120.82 105.38 None eca-rers2012/Problem06_label57.yml TIMEOUT 120.44 92.96 None eca-rers2012/Problem16_label24.yml TIMEOUT 120.66 108.25 None eca-rers2012/Problem19_label22.yml TIMEOUT 120.24 95.57 None eca-rers2012/Problem18_label55.yml TIMEOUT 120.82 105.41 None ---------------------------------------------------------------------------------------------------- Run set 1 done 1.21 958.89 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 14) ```
:white_check_mark: ReachSafety-Floats (5 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Floats/theta.2023-11-12_17-49-18.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Floats/theta.2023-11-12_17-49-18.results.SV-COMP24_unreach-call.ReachSafety-Floats.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Floats, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:49:18 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1245-552 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3116.984 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Floats Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- float-benchs/float_double.yml true 2.27 0.90 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml ERROR (solver error) 23.01 21.48 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.44 4.56 None floats-cdfpl/square_3.yml TIMEOUT 120.18 118.54 None floats-cbmc-regression/float11.yml true 2.68 1.02 None float-benchs/nan_double.yml false(unreach-call) 2.76 1.08 None float-benchs/Rump_double.yml true 42.44 40.92 None floats-cdfpl/newton_2_2.yml TIMEOUT 120.22 118.57 None floats-cdfpl/sine_3.yml TIMEOUT 120.22 118.58 None float-benchs/zonotope_3.c.v+lhb-reducer.yml TIMEOUT 120.22 117.70 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 80.11 544.80 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 5 correct true: 3 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 8 (max: 16) ```
:question: ReachSafety-Hardware (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Hardware/theta.2023-11-12_17-51-20.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Hardware/theta.2023-11-12_17-51-20.results.SV-COMP24_unreach-call.ReachSafety-Hardware.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Hardware, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:51:20 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1543-140 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3249.456 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Hardware Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------ btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml TIMEOUT 120.32 115.70 None btor2c-lazyMod.lup.2.prop1-func-interl.yml ERROR (solver error) 16.44 8.87 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml ERROR (solver error) 16.47 9.56 None btor2c-lazyMod.msmie.4.prop1-func-interl.yml ERROR (solver error) 98.12 81.07 None btor2c-lazyMod.brp.1.prop1-func-interl.yml ERROR (solver error) 9.23 3.53 None btor2c-lazyMod.brp2.5.prop3-back-serstep.yml ERROR (solver error) 12.30 5.84 None btor2c-lazyMod.shift_register_top_w64_d8_e0.yml TIMEOUT 120.24 117.70 None btor2c-lazyMod.sw_ball2004_1.yml ERROR (solver error) 3.20 1.22 None btor2c-lazyMod.at.7.prop1-back-serstep.yml ERROR (solver error) 17.87 10.00 None btor2c-lazyMod.peterson.7.prop1-func-interl.yml ERROR (solver error) 10.46 4.54 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 184.33 359.28 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 18) ```
:white_check_mark: ReachSafety-Heap (2 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Heap/theta.2023-11-12_17-48-39.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Heap/theta.2023-11-12_17-48-39.results.SV-COMP24_unreach-call.ReachSafety-Heap.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Heap, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:48:39 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az768-743 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3217.992 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Heap Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------- test09.yml ERROR (generic error) 1.98 0.84 None test15.yml ERROR (generic error) 2.00 0.86 None just_assert.yml true 1.96 0.82 None volatile_alias.yml ERROR (generic error) 1.99 0.85 None mutex_lock_int.c_1.yml ERROR (generic error) 2.03 0.86 None oomInt.yml true 2.35 0.95 None test16.yml ERROR (generic error) 1.97 0.85 None mutex_lock_int.yml ERROR (generic error) 2.05 0.89 None test18.yml ERROR (generic error) 2.07 0.89 None volatile_alias.c_1.yml ERROR (generic error) 2.02 0.86 None --------------------------------------------------------------------------------------- Run set 1 done 20.41 9.70 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 2 correct true: 2 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 8 Score: 4 (max: 19) ```
:question: ReachSafety-Loops (0 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Loops/theta.2023-11-12_17-50-16.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Loops/theta.2023-11-12_17-50-16.results.SV-COMP24_unreach-call.ReachSafety-Loops.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Loops, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:50:16 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az575-716 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3197.268 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Loops Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- nla-digbench/ps3-ll.yml TIMEOUT 120.45 114.41 None loop-crafted/simple_vardep_2.yml TIMEOUT 120.40 115.15 None nla-digbench-scaling/divbin_valuebound100.yml ERROR (server error) 7.80 3.75 None nla-digbench-scaling/mannadiv_valuebound50.yml TIMEOUT 120.71 109.70 None nla-digbench-scaling/mannadiv_unwindbound10.yml TIMEOUT 120.79 108.50 None loops-crafted-1/nested3-1_abstracted.yml ERROR (server error) 8.93 4.80 None nla-digbench-scaling/sqrt1-ll_valuebound2.yml TIMEOUT 120.37 114.42 None loop-acceleration/nested_1-2.yml TIMEOUT 120.57 113.29 None nla-digbench-scaling/hard-ll_valuebound2.yml TIMEOUT 120.77 108.87 None loop-invgen/down.yml TIMEOUT 120.72 109.61 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 17.70 904.36 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 10 Score: 0 (max: 18) ```
:white_check_mark: ReachSafety-Recursive (4 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Recursive/theta.2023-11-12_17-48-48.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Recursive/theta.2023-11-12_17-48-48.results.SV-COMP24_unreach-call.ReachSafety-Recursive.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Recursive, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:48:48 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az256-717 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: Intel Xeon Platinum 8272CL CPU @ 2.60GHz - cores: 2 - max frequency: 2593.906 MHz ram: 7258.226688 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Recursive Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------- recursive-simple/id_o100.yml TIMEOUT 120.21 117.21 None recursive-simple/id2_i5_o5-2.yml true 2.22 1.29 None recursive/recHanoi03-2.yml TIMEOUT 121.11 104.58 None recursive-simple/id_b3_o2-2.yml false(unreach-call) 2.75 1.61 None recursive-simple/afterrec-2.yml TIMEOUT 120.52 113.04 None recursive-simple/id_i10_o10-2.yml true 2.27 1.31 None recursive/EvenOdd03.yml false(unreach-call) 2.51 1.45 None recursive-simple/id_o200.yml TIMEOUT 120.31 114.26 None recursive/BallRajamani-SPIN2000-Fig1.yml TIMEOUT 121.23 101.68 None recursive-simple/id2_b3_o5.yml ERROR (solver error) 5.37 4.29 None --------------------------------------------------------------------------------------------------------- Run set 1 done 15.77 564.29 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 4 correct true: 2 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 6 Score: 6 (max: 15) ```
:white_check_mark: ReachSafety-Sequentialized (2 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Sequentialized/theta.2023-11-12_17-50-16.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-Sequentialized/theta.2023-11-12_17-50-16.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Sequentialized, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:50:16 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az581-725 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: Intel Xeon Platinum 8272CL CPU @ 2.60GHz - cores: 2 - max frequency: 2593.904 MHz ram: 7258.226688 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Sequentialized Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------- systemc/transmitter.12.cil.yml TIMEOUT 120.60 111.06 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT 121.11 106.73 None systemc/pipeline.cil-1.yml false(unreach-call) 37.40 26.97 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT 121.01 106.17 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml TIMEOUT 121.02 106.32 None seq-mthreaded/pals_opt-floodmax.5.ufo.BOUNDED-10.pals.yml TIMEOUT 121.11 105.40 None systemc/toy.cil.yml TIMEOUT 120.35 112.90 None seq-mthreaded/pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.yml TIMEOUT 121.12 106.84 None systemc/mem_slave_tlm.5.cil.yml true 30.76 22.11 None systemc/token_ring.09.cil-1.yml TIMEOUT 120.73 106.48 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 69.24 915.66 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 2 correct true: 1 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 8 Score: 3 (max: 15) ```
:white_check_mark: ReachSafety-XCSP (2 / 0 / 10) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-XCSP/theta.2023-11-12_17-48-15.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xcfa-refactor-benchexec-test/BenchexecResults-ReachSafety-XCSP/theta.2023-11-12_17-48-15.results.SV-COMP24_unreach-call.ReachSafety-XCSP.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-XCSP, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Sun, 2023-11-12 17:48:15 UTC tool: Theta 5.0.0 tool executable: theta/theta-start.sh options: --witness-only --portfolio COMPLEX --loglevel RESULT resource limits: - time: 120 s hardware requirements: - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az770-151 os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.076 MHz ram: 16757.796864 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-XCSP Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------- CostasArray-14.yml TIMEOUT 120.39 113.51 None Dubois-025.yml ERROR (solver error) 25.95 21.55 None aim-100-2-0-unsat-4.yml ERROR (server error) 10.68 5.48 None AllInterval-014.yml TIMEOUT 120.26 116.50 None AllInterval-005.yml false(unreach-call) 4.45 1.60 None aim-100-1-6-unsat-4.yml ERROR (server error) 11.74 6.88 None AllInterval-012.yml TIMEOUT 120.26 117.06 None Dubois-100.yml TIMEOUT 120.46 112.16 None AllInterval-009.yml false(unreach-call) 8.23 3.84 None aim-200-1-6-unsat-2.yml ERROR (server error) 20.49 13.93 None ---------------------------------------------------------------------------------------- Run set 1 done 82.07 513.95 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 10 Files correct: 2 correct true: 0 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 8 Score: 2 (max: 15) ```