Allow `$` in xsts variable names

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/xstsvarname/BenchexecResults-ConcurrencySafety-Main/theta.2024-07-31_10-35-25.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ConcurrencySafety-Main/theta.2024-07-31_10-35-25.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: Wed, 2024-07-31 10:35:25 UTC tool: Theta 6.2.3 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-az1536-525 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2592.775 MHz ram: 16757.338112 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 10.81 5.19 None pthread-atomic/read_write_lock-1.yml true 10.93 4.12 None pthread-wmm/rfi003_tso.yml TIMEOUT 120.81 89.13 None pthread/lazy01.yml false(unreach-call) 7.08 3.07 None pthread-wmm/mix000.oepc.yml false(unreach-call) 18.39 6.95 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 47.30 109.19 - 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/xstsvarname/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-07-31_10-35-18.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-07-31_10-35-18.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: Wed, 2024-07-31 10:35:18 UTC tool: Theta 6.2.3 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-az849-821 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3010.912 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 10.73 5.22 None pthread-atomic/read_write_lock-1.yml true 8.64 3.41 None pthread-wmm/rfi003_tso.yml true 13.82 5.75 None pthread/lazy01.yml true 6.97 3.04 None pthread-wmm/mix000.oepc.yml true 14.27 5.84 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 54.41 23.78 - 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/xstsvarname/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-07-31_10-35-25.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-07-31_10-35-25.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: Wed, 2024-07-31 10:35:25 UTC tool: Theta 6.2.3 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-az525-159 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3149.845 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 12.01 5.47 None pthread-atomic/read_write_lock-1.yml true 9.54 3.72 None pthread-wmm/rfi003_tso.yml true 16.17 6.51 None pthread/lazy01.yml true 7.84 3.32 None pthread-wmm/mix000.oepc.yml true 15.08 6.18 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 60.61 25.74 - 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/xstsvarname/BenchexecResults-NoDataRace-Main/theta.2024-07-31_10-35-30.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-NoDataRace-Main/theta.2024-07-31_10-35-30.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: Wed, 2024-07-31 10:35:30 UTC tool: Theta 6.2.3 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-az849-821 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2813.461 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.58 5.13 None pthread-atomic/read_write_lock-1.yml true 11.50 4.31 None pthread-wmm/rfi003_tso.yml true 17.95 7.02 None pthread/lazy01.yml true 7.87 3.24 None pthread-wmm/mix000.oepc.yml true 17.73 6.91 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 65.61 27.14 - 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/xstsvarname/BenchexecResults-ReachSafety-Arrays/theta.2024-07-31_10-33-54.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Arrays/theta.2024-07-31_10-33-54.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: Wed, 2024-07-31 10:33:54 UTC tool: Theta 6.2.3 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-az1144-461 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3193.482 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.46 161.00 None array-crafted/mapavg4.yml TIMEOUT 77.56 161.02 None array-programs/copysome2-1.yml TIMEOUT 78.15 161.02 None array-examples/sanfoundry_24-1.yml true 12.01 103.28 None array-multidimensional/max-2-u.yml ERROR (frontend failed) 1.79 0.76 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 14.15 588.31 - 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/xstsvarname/BenchexecResults-ReachSafety-BitVectors/theta.2024-07-31_10-32-51.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-BitVectors/theta.2024-07-31_10-32-51.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: Wed, 2024-07-31 10:32:51 UTC tool: Theta 6.2.3 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-az1014-921 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3084.605 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 7.40 3.11 None bitvector/soft_float_1-3a.c.cil.yml false(unreach-call) 34.85 18.62 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 5.34 3.01 None bitvector/sum02-1.yml Parsing OK 38.05 19.28 None bitvector-loops/diamond_2-1.yml TIMEOUT 121.04 109.51 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 80.14 154.16 - 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/xstsvarname/BenchexecResults-ReachSafety-Combinations/theta.2024-07-31_10-34-32.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Combinations/theta.2024-07-31_10-34-32.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: Wed, 2024-07-31 10:34:32 UTC tool: Theta 6.2.3 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-az1424-702 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3219.234 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.77 71.87 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.36 94.79 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 120.29 107.25 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.39 94.75 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 120.62 67.85 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 0.61 437.63 - 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/xstsvarname/BenchexecResults-ReachSafety-ControlFlow/theta.2024-07-31_10-33-00.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-ControlFlow/theta.2024-07-31_10-33-00.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: Wed, 2024-07-31 10:33:00 UTC tool: Theta 6.2.3 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-az881-897 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2941.616 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) 4.34 1.55 None locks/test_locks_11.yml TIMEOUT 123.45 103.36 None locks/test_locks_5.yml true 14.56 5.50 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml ERROR (frontend failed) 4.81 1.73 None longjmp/68-longjmp_11-counting-return_true.yml ERROR (frontend failed) 2.08 0.86 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 25.87 113.62 - 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/xstsvarname/BenchexecResults-ReachSafety-ECA/theta.2024-07-31_10-36-11.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-ECA/theta.2024-07-31_10-36-11.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: Wed, 2024-07-31 10:36:11 UTC tool: Theta 6.2.3 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-az1110-82 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3227.835 MHz ram: 16757.342208000002 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.24 77.87 None eca-rers2012/Problem06_label11.yml TIMEOUT 120.16 75.27 None eca-programs/Problem101_label07.yml TIMEOUT 121.07 74.44 None eca-rers2012/Problem05_label44.yml TIMEOUT 120.27 72.84 None eca-rers2012/Problem04_label05.yml TIMEOUT 120.94 75.25 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.59 378.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: 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/xstsvarname/BenchexecResults-ReachSafety-Floats/theta.2024-07-31_10-35-36.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Floats/theta.2024-07-31_10-35-36.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: Wed, 2024-07-31 10:35:36 UTC tool: Theta 6.2.3 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-az1391-55 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3183.503 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.76 2.93 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml TIMEOUT 120.45 112.56 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.47 3.13 None floats-cdfpl/square_3.yml false(unreach-call) 74.76 71.19 None floats-cbmc-regression/float11.yml true 5.17 2.91 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 24.18 193.75 - 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/xstsvarname/BenchexecResults-ReachSafety-Hardware/theta.2024-07-31_10-36-09.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Hardware/theta.2024-07-31_10-36-09.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: Wed, 2024-07-31 10:36:09 UTC tool: Theta 6.2.3 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-az1380-767 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2991.517 MHz ram: 16757.342208000002 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.62 111.91 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT 120.45 99.09 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT 120.45 94.82 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT 120.46 94.47 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml TIMEOUT 120.56 83.42 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 0.62 485.93 - 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/xstsvarname/BenchexecResults-ReachSafety-Heap/theta.2024-07-31_10-33-21.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Heap/theta.2024-07-31_10-33-21.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: Wed, 2024-07-31 10:33:21 UTC tool: Theta 6.2.3 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-493 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.254 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.77 4.81 None test15.yml true 8.73 4.59 None just_assert.yml true 5.65 2.72 None volatile_alias.yml true 7.99 4.17 None mutex_lock_int.c_1.yml true 8.82 4.49 None --------------------------------------------------------------------------------------- Run set 1 done 40.92 21.31 - 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/xstsvarname/BenchexecResults-ReachSafety-Loops/theta.2024-07-31_10-35-04.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Loops/theta.2024-07-31_10-35-04.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: Wed, 2024-07-31 10:35:04 UTC tool: Theta 6.2.3 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-az735-305 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2730.568 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.46 106.93 None loop-crafted/simple_vardep_2.yml TIMEOUT 120.75 109.99 None nla-digbench-scaling/divbin_valuebound100.yml TIMEOUT 120.67 107.38 None nla-digbench-scaling/mannadiv_valuebound50.yml true 22.60 9.97 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 28.69 12.59 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 51.52 347.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: 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/xstsvarname/BenchexecResults-ReachSafety-Recursive/theta.2024-07-31_10-33-12.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Recursive/theta.2024-07-31_10-33-12.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: Wed, 2024-07-31 10:33:12 UTC tool: Theta 6.2.3 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-az2021-574 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3197.488 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 16.94 7.18 None recursive-simple/id2_i5_o5-2.yml true 13.07 5.07 None recursified_nla-digbench/recursified_geo2-ll.yml TIMEOUT 33.37 161.03 None recursive/recHanoi03-2.yml TIMEOUT 120.16 92.90 None recursified_nla-digbench/recursified_lcm2.yml TIMEOUT 120.37 113.95 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 30.32 381.51 - 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/xstsvarname/BenchexecResults-ReachSafety-Sequentialized/theta.2024-07-31_10-34-16.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-Sequentialized/theta.2024-07-31_10-34-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: Wed, 2024-07-31 10:34:16 UTC tool: Theta 6.2.3 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-az887-816 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3249.728 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 120.22 107.88 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT 120.41 93.41 None systemc/pipeline.cil-1.yml TIMEOUT 120.59 103.95 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT 120.56 93.74 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml false(unreach-call) 103.36 66.99 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 102.07 467.39 - 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/xstsvarname/BenchexecResults-ReachSafety-XCSP/theta.2024-07-31_10-32-55.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/xstsvarname/BenchexecResults-ReachSafety-XCSP/theta.2024-07-31_10-32-55.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: Wed, 2024-07-31 10:32:55 UTC tool: Theta 6.2.3 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-az885-996 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2964.501 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.06 107.61 None Dubois-025.yml TIMEOUT 120.20 107.84 None aim-100-2-0-unsat-4.yml TIMEOUT 120.43 105.65 None AllInterval-014.yml TIMEOUT 120.85 109.35 None AllInterval-005.yml TIMEOUT 120.37 105.57 None ---------------------------------------------------------------------------------------- Run set 1 done 0.60 537.05 - 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) ```

ftsrg / theta

Allow `$` in xsts variable names #287

Quality Gate passed