Adding smoke test to xcfa-cli

[leventeBajczi]

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

[sonarqubecloud]

Kudos, SonarCloud Quality Gate passed!   

0 Bugs
0 Vulnerabilities
0 Security Hotspots
0 Code Smells

No Coverage information
No Duplication information

[github-actions]

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

❓ ConcurrencySafety-Main (0 / 0 / 10)

table-generator output: HTML/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)

❓ ConcurrencySafety-MemSafety (0 / 0 / 10)

table-generator output: HTML/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)

❓ ConcurrencySafety-NoOverflows (0 / 0 / 10)

table-generator output: HTML/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)

❓ NoDataRace-Main (0 / 0 / 10)

table-generator output: HTML/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)

❓ ReachSafety-Arrays (0 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-BitVectors (6 / 0 / 10)

table-generator output: HTML/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)

❓ ReachSafety-Combinations (0 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-ControlFlow (7 / 0 / 10)

table-generator output: HTML/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)

❓ ReachSafety-ECA (0 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-Floats (5 / 0 / 10)

table-generator output: HTML/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)

❓ ReachSafety-Hardware (0 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-Heap (2 / 0 / 10)

table-generator output: HTML/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)

❓ ReachSafety-Loops (0 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-Recursive (4 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-Sequentialized (2 / 0 / 10)

table-generator output: HTML/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)

✅ ReachSafety-XCSP (2 / 0 / 10)

table-generator output: HTML/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)