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

SMTLIB integration fixes #271

Closed mondokm closed 5 months ago

mondokm commented 5 months ago

This PR fixes some of the JavaSmt-unrelated issues listed in #268 and adds support for newer versions of some solvers:

github-actions[bot] commented 5 months ago

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

:white_check_mark: ConcurrencySafety-Main (3 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ConcurrencySafety-Main/theta.2024-06-24_13-30-12.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ConcurrencySafety-Main/theta.2024-06-24_13-30-12.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: Mon, 2024-06-24 13:30:12 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az570-320 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3182.976 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ConcurrencySafety-Main Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 11.01 5.03 None pthread-atomic/read_write_lock-1.yml true 11.25 4.24 None pthread-wmm/rfi003_tso.yml TIMEOUT 120.60 90.18 None pthread/lazy01.yml false(unreach-call) 7.54 3.23 None pthread-wmm/mix000.oepc.yml false(unreach-call) 19.94 7.56 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 49.83 110.96 - 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: 5 Files correct: 3 correct true: 1 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2 Score: 4 (max: 8) ```
:white_check_mark: ConcurrencySafety-MemSafety (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-06-24_13-30-08.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-06-24_13-30-08.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: Mon, 2024-06-24 13:30:08 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1108-192 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3022.179 MHz ram: 16757.342208000002 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 '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 11.02 5.23 None pthread-atomic/read_write_lock-1.yml true 9.47 3.73 None pthread-wmm/rfi003_tso.yml true 15.35 6.18 None pthread/lazy01.yml true 7.38 3.15 None pthread-wmm/mix000.oepc.yml true 13.74 5.62 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 56.94 24.44 - Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: ConcurrencySafety-NoOverflows (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-06-24_13-30-03.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-06-24_13-30-03.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: Mon, 2024-06-24 13:30:03 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1113-373 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.352 MHz ram: 16757.342208000002 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 '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 11.69 5.33 None pthread-atomic/read_write_lock-1.yml true 8.79 3.48 None pthread-wmm/rfi003_tso.yml true 16.52 6.57 None pthread/lazy01.yml true 7.85 3.29 None pthread-wmm/mix000.oepc.yml true 14.95 6.17 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 59.77 25.37 - SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: NoDataRace-Main (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-NoDataRace-Main/theta.2024-06-24_13-30-15.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-NoDataRace-Main/theta.2024-06-24_13-30-15.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: Mon, 2024-06-24 13:30:15 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1499-511 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3129.272 MHz ram: 16757.342208000002 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 '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 10.97 5.20 None pthread-atomic/read_write_lock-1.yml true 11.46 4.33 None pthread-wmm/rfi003_tso.yml true 18.00 7.08 None pthread/lazy01.yml true 7.30 3.12 None pthread-wmm/mix000.oepc.yml true 17.70 6.97 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 65.39 27.23 - 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: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: ReachSafety-Arrays (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Arrays/theta.2024-06-24_13-28-33.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Arrays/theta.2024-06-24_13-28-33.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: Mon, 2024-06-24 13:28:33 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1113-373 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3238.293 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Arrays Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------------- array-examples/standard_partition_ground-2.yml TIMEOUT 76.16 161.00 None array-crafted/mapavg4.yml TIMEOUT 77.18 161.02 None array-programs/copysome2-1.yml TIMEOUT 77.92 161.02 None array-examples/sanfoundry_24-1.yml true 11.84 103.26 None array-multidimensional/max-2-u.yml ERROR (frontend failed) 1.76 0.73 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 13.95 588.27 - 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: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 10) ```
:white_check_mark: ReachSafety-BitVectors (3 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-BitVectors/theta.2024-06-24_13-27-31.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-BitVectors/theta.2024-06-24_13-27-31.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: Mon, 2024-06-24 13:27:31 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1456-774 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.209 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-BitVectors Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------ bitvector/gcd_4.yml true 6.65 2.90 None bitvector/soft_float_1-3a.c.cil.yml false(unreach-call) 31.82 17.17 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 5.02 2.54 None bitvector/sum02-1.yml Parsing OK 36.49 18.39 None bitvector-loops/diamond_2-1.yml TIMEOUT 121.74 86.02 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 74.65 127.64 - 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: 5 Files correct: 3 correct true: 1 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2 Score: 4 (max: 6) ```
:question: ReachSafety-Combinations (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Combinations/theta.2024-06-24_13-32-10.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Combinations/theta.2024-06-24_13-32-10.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: Mon, 2024-06-24 13:32:10 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1247-446 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3216.874 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Combinations Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------------- pc_sfifo_3.cil+token_ring.02.cil-2.yml TIMEOUT 120.38 74.60 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.34 95.11 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 120.15 107.63 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.58 92.16 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 120.96 69.77 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 0.59 440.81 - 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: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 5) ```
:white_check_mark: ReachSafety-ControlFlow (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-ControlFlow/theta.2024-06-24_13-27-39.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-ControlFlow/theta.2024-06-24_13-27-39.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: Mon, 2024-06-24 13:27:39 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az840-896 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2694.23 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ControlFlow Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------- longjmp/68-longjmp_18-simple-else_unknown_1_pos.yml ERROR (frontend failed) 3.77 1.34 None locks/test_locks_11.yml TIMEOUT 122.64 102.80 None locks/test_locks_5.yml true 13.73 5.34 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml ERROR (frontend failed) 4.30 1.53 None longjmp/68-longjmp_11-counting-return_true.yml ERROR (frontend failed) 2.09 0.85 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 23.35 112.50 - 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: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 8) ```
:question: ReachSafety-ECA (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-ECA/theta.2024-06-24_13-35-19.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-ECA/theta.2024-06-24_13-35-19.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: Mon, 2024-06-24 13:35:19 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az698-74 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3240.134 MHz ram: 16757.338112 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ECA Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------- eca-rers2012/Problem06_label18.yml TIMEOUT 122.07 79.22 None eca-rers2012/Problem06_label11.yml TIMEOUT 121.02 76.15 None eca-programs/Problem101_label07.yml TIMEOUT 121.27 71.89 None eca-rers2012/Problem05_label44.yml TIMEOUT 120.43 72.50 None eca-rers2012/Problem04_label05.yml TIMEOUT 121.02 73.07 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.60 375.76 - 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: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 7) ```
:white_check_mark: ReachSafety-Floats (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Floats/theta.2024-06-24_13-30-16.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Floats/theta.2024-06-24_13-30-16.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: Mon, 2024-06-24 13:30:16 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1778-473 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3279.904 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Floats Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- float-benchs/float_double.yml true 5.43 2.82 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml TIMEOUT 120.42 113.11 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.02 3.00 None floats-cdfpl/square_3.yml false(unreach-call) 75.68 71.51 None floats-cbmc-regression/float11.yml true 5.26 2.76 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 92.40 194.22 - 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: 5 Files correct: 4 correct true: 2 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 6 (max: 8) ```
:question: ReachSafety-Hardware (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Hardware/theta.2024-06-24_13-30-47.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Hardware/theta.2024-06-24_13-30-47.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: Mon, 2024-06-24 13:30:47 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az736-148 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3244.475 MHz ram: 16757.334016 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Hardware Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------ btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml TIMEOUT 120.60 111.71 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT 120.42 99.25 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT 120.38 95.87 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT 123.11 94.63 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml TIMEOUT 120.67 86.80 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 0.59 490.88 - 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: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 9) ```
:white_check_mark: ReachSafety-Heap (5 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Heap/theta.2024-06-24_13-28-01.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Heap/theta.2024-06-24_13-28-01.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: Mon, 2024-06-24 13:28:01 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az575-755 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.175 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Heap Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------- test09.yml true 9.89 4.71 None test15.yml true 8.76 4.28 None just_assert.yml true 5.45 2.58 None volatile_alias.yml true 8.01 4.18 None mutex_lock_int.c_1.yml true 8.97 4.37 None --------------------------------------------------------------------------------------- Run set 1 done 41.06 20.64 - 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: 5 Files correct: 5 correct true: 5 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 0 Score: 10 (max: 10) ```
:white_check_mark: ReachSafety-Loops (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Loops/theta.2024-06-24_13-30-01.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Loops/theta.2024-06-24_13-30-01.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: Mon, 2024-06-24 13:30:01 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1766-97 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2871.636 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Loops Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- nla-digbench/ps3-ll.yml TIMEOUT 120.40 107.17 None loop-crafted/simple_vardep_2.yml TIMEOUT 120.91 109.61 None nla-digbench-scaling/divbin_valuebound100.yml TIMEOUT 120.68 107.28 None nla-digbench-scaling/mannadiv_valuebound50.yml true 22.96 10.34 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 28.98 12.38 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 52.18 347.60 - 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: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 9) ```
:white_check_mark: ReachSafety-Recursive (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Recursive/theta.2024-06-24_13-27-51.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Recursive/theta.2024-06-24_13-27-51.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: Mon, 2024-06-24 13:27:51 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az693-187 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3203.96 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Recursive Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------------- recursive-simple/id_o100.yml Parsing OK 18.26 7.31 None recursive-simple/id2_i5_o5-2.yml true 14.29 5.33 None recursified_nla-digbench/recursified_geo2-ll.yml TIMEOUT 35.51 161.02 None recursive/recHanoi03-2.yml TIMEOUT 120.37 90.21 None recursified_nla-digbench/recursified_lcm2.yml TIMEOUT 120.38 113.78 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 32.88 379.02 - 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: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 9) ```
:white_check_mark: ReachSafety-Sequentialized (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Sequentialized/theta.2024-06-24_13-29-14.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-Sequentialized/theta.2024-06-24_13-29-14.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: Mon, 2024-06-24 13:29:14 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az914-840 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2595.373 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Sequentialized Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------- systemc/transmitter.12.cil.yml TIMEOUT 121.04 109.73 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT 120.36 94.14 None systemc/pipeline.cil-1.yml TIMEOUT 120.37 105.61 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT 120.66 94.37 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml false(unreach-call) 104.26 66.80 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 103.02 471.69 - 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: 5 Files correct: 1 correct true: 0 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 1 (max: 6) ```
:question: ReachSafety-XCSP (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-XCSP/theta.2024-06-24_13-27-36.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/smtlib-fixes/BenchexecResults-ReachSafety-XCSP/theta.2024-06-24_13-27-36.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: Mon, 2024-06-24 13:27:36 UTC tool: Theta 5.2.1 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az738-293 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3222.521 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-XCSP Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------- CostasArray-14.yml TIMEOUT 120.17 105.62 None Dubois-025.yml TIMEOUT 120.30 106.39 None aim-100-2-0-unsat-4.yml TIMEOUT 120.17 107.42 None AllInterval-014.yml TIMEOUT 120.43 105.14 None AllInterval-005.yml TIMEOUT 120.30 105.07 None ---------------------------------------------------------------------------------------- Run set 1 done 0.61 530.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: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 7) ```