Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

K induction and IMC #243

Merged
merged 46 commits into from
Nov 19, 2023
Merged

K induction and IMC #243

merged 46 commits into from
Nov 19, 2023

Conversation

leventeBajczi
Copy link
Contributor

@leventeBajczi leventeBajczi force-pushed the xcfa-refactor-kind_imc branch 2 times, most recently from ff8bc3e to 077a6ce Compare November 16, 2023 14:51
mondokz and others added 28 commits November 17, 2023 20:58
@mondokz @leventeBajczi
Create Xsts_K_induction.java
8d97b25
@leventeBajczi
Removed tests
7be5ad5
@mondokz @leventeBajczi
fixed
ecd091c
@mondokz @leventeBajczi
Update KIndChecker.java
8d6cc26
@mondokz @leventeBajczi
Removed tests
2b58777
@mondokz @leventeBajczi
Update Xsts_K_induction.java
4bcc183
@mondokz @leventeBajczi
Not allowing dependency on xsts from common/analysis
f10842d
@mondokz @leventeBajczi
dependency-fix
f2f405a
@mondokz @leventeBajczi
bohoc
241b913 
nem mukodik,
sok kerdes
index???????
@mondokz @leventeBajczi
fixed indexes
e265420
@mondokz @leventeBajczi
loopcheck fixed, xsts input fixed
702bb72
@mondokz @leventeBajczi
xsts cli with k-induction added
bf22867
@mondokz @leventeBajczi
added cfa and sts k-induction
d9e688d
@mondokm @leventeBajczi
Refactored CFA KInduction handling
1abff16
@mondokm @leventeBajczi
Fixed benchmarking
90038ce
@mondokz @leventeBajczi
added incrementality
a6ccd76
@mondokm @leventeBajczi
Fixed benchmarking
945bbf6
@mondokz @leventeBajczi
added imc
049b30b
@mondokz @leventeBajczi
added k-induction and imc support to XCFA
f0ca7d8
@mondokz @leventeBajczi
fixed minor issues
8234646
@mondokz @leventeBajczi
fixed missing ;
98fe55e
@mondokz @leventeBajczi
introduced monolitic interface
1c9140f 
+ changed cli-s based on new interface
@mondokz @leventeBajczi
fixed missing propexpr's
d5bde8e
@leventeBajczi
Added solver choice to kind and imc
89a31d3
@leventeBajczi
Delete subprojects/xcfa/xcfa-cli/witness.graphml
ec7cf48
@leventeBajczi
Added back XSTS cli
37fcab2
@leventeBajczi
sanitized branch
54984bb
@thetabotmaintainer @leventeBajczi
Reformatted code
05eedd4
@leventeBajczi leventeBajczi marked this pull request as ready for review November 19, 2023 13:09
@leventeBajczi leventeBajczi merged commit b62d991 into xcfa-refactor Nov 19, 2023
7 of 10 checks passed
@leventeBajczi leventeBajczi deleted the xcfa-refactor-kind_imc branch November 19, 2023 13:22
@sonarqubecloud SonarQubeCloud
Copy link

Kudos, SonarCloud Quality Gate passed!    Quality Gate passed

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

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

@github-actions GitHub Actions
Copy link

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

✅ ConcurrencySafety-Main (8 / 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-19 13:37:33 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-az585-782
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3230.371 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-ext/18_read_write_lock-pthread.yml                           ERROR (frontend failed)          3.77        1.42        None
pthread-atomic/read_write_lock-1.yml                                 true                            13.84        5.43        None
pthread-wmm/rfi003_tso.yml                                           true                            33.72       14.62        None
pthread/lazy01.yml                                                   false(unreach-call)              9.71        4.37        None
pthread-wmm/mix000.oepc.yml                                          false(unreach-call)             15.32        5.77        None
goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.yml    false(unreach-call)             10.83        4.69        None
pthread-wmm/safe032_tso.yml                                          true                            12.10        5.06        None
goblint-regression/13-privatized_37-traces-ex-4_true.yml             true                             9.80        4.39        None
pthread-C-DAC/pthread-demo-datarace-3.yml                            ERROR (frontend failed)          5.31        1.95        None
goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.yml    true                             9.57        4.33        None
----------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                            done                           123.98       53.06           -


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:               8
    correct true:        5
    correct false:       3
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                13 (max: 16)
✅ ConcurrencySafety-MemSafety (8 / 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-19 13:37: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-az738-414
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.491 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-ext/18_read_write_lock-pthread.yml                           ERROR (frontend failed)          3.77        1.43        None
pthread-atomic/read_write_lock-1.yml                                 true                            10.90        4.65        None
pthread-wmm/rfi003_tso.yml                                           true                            11.99        5.05        None
pthread/lazy01.yml                                                   true                             9.27        4.24        None
pthread-wmm/mix000.oepc.yml                                          true                            11.59        4.96        None
goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.yml    true                            10.18        4.39        None
pthread-wmm/safe032_tso.yml                                          true                            10.13        4.47        None
goblint-regression/13-privatized_37-traces-ex-4_true.yml             true                             8.73        4.11        None
pthread-C-DAC/pthread-demo-datarace-3.yml                            ERROR (frontend failed)          5.16        1.90        None
goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.yml    true                             9.65        4.36        None
----------------------------------------------------------------------------------------------------------------------------------
Run set 4                                                            done                            91.39       40.60           -

Statistics:             10 Files
  correct:               8
    correct true:        8
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                16 (max: 20)
✅ ConcurrencySafety-NoOverflows (8 / 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-19 13:37:32 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-256
os:                      Linux-6.2.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3246.643 MHz
ram:                     16757.78048 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-ext/18_read_write_lock-pthread.yml                           ERROR (frontend failed)          3.41        1.29        None
pthread-atomic/read_write_lock-1.yml                                 true                            11.69        4.96        None
pthread-wmm/rfi003_tso.yml                                           true                            12.37        5.09        None
pthread/lazy01.yml                                                   true                             9.89        4.28        None
pthread-wmm/mix000.oepc.yml                                          true                            12.05        5.09        None
goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.yml    true                             9.82        4.33        None
pthread-wmm/safe032_tso.yml                                          true                            10.75        4.59        None
goblint-regression/13-privatized_37-traces-ex-4_true.yml             true                             9.26        4.28        None
pthread-C-DAC/pthread-demo-datarace-3.yml                            ERROR (frontend failed)          5.99        2.17        None
goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.yml    true                            10.14        4.51        None
----------------------------------------------------------------------------------------------------------------------------------
Run set 3                                                            done                            95.37       41.64           -


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:             10 Files
  correct:               8
    correct true:        8
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                16 (max: 20)
✅ NoDataRace-Main (8 / 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-19 13:37:37 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-az891-357
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3244.144 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.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-ext/18_read_write_lock-pthread.yml                           ERROR (frontend failed)          4.08        1.52        None
pthread-atomic/read_write_lock-1.yml                                 true                            15.51        5.89        None
pthread-wmm/rfi003_tso.yml                                           true                            15.70        6.05        None
pthread/lazy01.yml                                                   true                             9.72        4.28        None
pthread-wmm/mix000.oepc.yml                                          true                            14.72        5.81        None
goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.yml    true                             8.87        4.32        None
pthread-wmm/safe032_tso.yml                                          true                            11.87        5.11        None
goblint-regression/13-privatized_37-traces-ex-4_true.yml             true                            10.04        4.41        None
pthread-C-DAC/pthread-demo-datarace-3.yml                            ERROR (frontend failed)          6.60        2.36        None
goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.yml    true                             9.52        4.31        None
----------------------------------------------------------------------------------------------------------------------------------
Run set 2                                                            done                           106.63       45.10           -


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:               8
    correct true:        8
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                16 (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-19 13:36:13 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-az1385-972
os:                      Linux-6.2.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3239.31 MHz
ram:                     16757.78048 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                      ERROR (portfolio error)          2.16        0.90        None
array-crafted/mapavg4.yml                                           ERROR (portfolio error)          2.16        0.91        None
array-programs/copysome2-1.yml                                      ERROR (portfolio error)          2.17        0.91        None
array-examples/sanfoundry_24-1.yml                                  ERROR (portfolio error)          2.10        0.90        None
array-multidimensional/max-2-u.yml                                  ERROR (portfolio error)          2.09        0.87        None
array-examples/sorting_bubblesort_ground-1.yml                      ERROR (portfolio error)          2.15        0.90        None
array-crafted/bAnd2.yml                                             ERROR (portfolio error)          2.18        0.90        None
array-multidimensional/rev-2-n-u.yml                                ERROR (portfolio error)          2.09        0.88        None
array-examples/data_structures_set_multi_proc_trivial_ground.yml    ERROR (portfolio error)          2.26        0.94        None
array-patterns/array21_pattern.yml                                  ERROR (portfolio error)          2.17        0.90        None
---------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                           done                            21.54       10.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:             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-BitVectors (3 / 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-19 13:35:05 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-az520-462
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3245.377 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                             8.86        3.63        None
bitvector/soft_float_1-3a.c.cil.yml            ERROR (portfolio error)         11.25        5.56        None
bitvector-regression/integerpromotion-3.yml    ERROR (portfolio error)          6.52        4.12        None
bitvector/sum02-1.yml                          ERROR (portfolio error)         23.32       10.92        None
bitvector-loops/diamond_2-1.yml                ERROR (portfolio error)         30.94       12.97        None
bitvector/gcd_1.yml                            ERROR (portfolio error)         17.57        8.89        None
bitvector-regression/signextension-1.yml       false(unreach-call)              6.93        3.66        None
bitvector/s3_srvr_3a.BV.c.cil.yml              ERROR (portfolio error)         13.14        5.84        None
bitvector-regression/signextension2-2.yml      false(unreach-call)              6.94        3.62        None
bitvector/interleave_bits.yml                  ERROR (portfolio error)          7.85        4.50        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                           133.32       64.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:             10 Files
  correct:               3
    correct true:        1
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               7
  Score:                 4 (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-19 13:36:40 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-az659-361
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3240.952 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.81      104.67        None
Problem05_label47+token_ring.02.cil-1.yml                       TIMEOUT                        120.30       73.00        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                          TIMEOUT                        120.23       95.09        None
Problem05_label45+token_ring.01.cil-2.yml                       TIMEOUT                        120.13       69.01        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml           TIMEOUT                        121.25       55.04        None
pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label04.yml    TIMEOUT                        121.88       55.02        None
gcd_3+newton_3_8.yml                                            ERROR (portfolio error)         10.52        5.16        None
pals_lcr.4_overflow.ufo.UNBOUNDED.pals+Problem12_label09.yml    TIMEOUT                        120.88       54.64        None
gcd_2+newton_3_3.yml                                            ERROR (portfolio error)         10.58        5.15        None
pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label09.yml            TIMEOUT                        120.91       84.91        None
-----------------------------------------------------------------------------------------------------------------------------
Run set 1                                                       done                            22.04      605.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:             10 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:              10
  Score:                 0 (max: 12)
✅ ReachSafety-ControlFlow (2 / 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-19 13:35:07 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-az1542-940
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.398 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
------------------------------------------------------------------------------------------------------------------------
longjmp/68-longjmp_18-simple-else_unknown_1_pos.yml        ERROR (frontend failed)          3.43        1.33        None
locks/test_locks_11.yml                                    TIMEOUT                        120.66      110.61        None
locks/test_locks_5.yml                                     true                            11.67        4.97        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml        ERROR (frontend failed)          3.95        1.48        None
longjmp/68-longjmp_11-counting-return_true.yml             ERROR (frontend failed)          1.61        0.77        None
locks/test_locks_9.yml                                     true                           108.50       91.06        None
longjmp/68-longjmp_12-counting-global_unknown_1_pos.yml    ERROR (frontend failed)          1.63        0.78        None
longjmp/68-longjmp_11-counting-return_unknown_1_neg.yml    ERROR (frontend failed)          1.73        0.81        None
locks/test_locks_14-2.yml                                  TIMEOUT                        121.86       99.52        None
longjmp/68-longjmp_04-counting-local_true.yml              ERROR (frontend failed)          1.68        0.79        None
------------------------------------------------------------------------------------------------------------------------
Run set 1                                                  done                           134.45      313.77           -


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: 15)
❓ 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-19 13:38: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-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:         3078.734 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                        121.11       74.58        None
eca-rers2012/Problem06_label11.yml     TIMEOUT                        120.16       68.90        None
eca-programs/Problem101_label07.yml    TIMEOUT                        121.61       70.38        None
eca-rers2012/Problem05_label44.yml     TIMEOUT                        122.96       71.38        None
eca-rers2012/Problem04_label05.yml     TIMEOUT                        120.67       73.07        None
eca-rers2012/Problem18_label36.yml     TIMEOUT                        120.60       62.51        None
eca-rers2012/Problem06_label57.yml     TIMEOUT                        120.81       65.04        None
eca-rers2012/Problem16_label24.yml     TIMEOUT                        120.65       92.23        None
eca-rers2012/Problem19_label22.yml     TIMEOUT                        121.14       72.57        None
eca-rers2012/Problem18_label55.yml     TIMEOUT                        120.67       57.37        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             1.21      711.59           -


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 (0 / 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-19 13:38:05 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-az1148-398
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2959.577 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                      ERROR (portfolio error)          6.66        4.17        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    ERROR (portfolio error)          7.30        4.35        None
float-benchs/float_int_inv_square.yml              ERROR (portfolio error)          7.46        4.32        None
floats-cdfpl/square_3.yml                          ERROR (portfolio error)          7.04        4.27        None
floats-cbmc-regression/float11.yml                 ERROR (portfolio error)          6.88        4.34        None
float-benchs/nan_double.yml                        ERROR (portfolio error)          6.65        4.19        None
float-benchs/Rump_double.yml                       ERROR (portfolio error)          6.91        4.21        None
floats-cdfpl/newton_2_2.yml                        ERROR (portfolio error)          7.90        4.45        None
floats-cdfpl/sine_3.yml                            ERROR (portfolio error)          7.32        4.30        None
float-benchs/zonotope_3.c.v+lhb-reducer.yml        ERROR (portfolio error)         12.07        5.51        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            76.19       45.15           -


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: 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-19 13:38:24 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-az1205-844
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2631.654 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.63        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml      ERROR (portfolio error)         38.56       22.37        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml      ERROR (portfolio error)         44.02       22.70        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml             ERROR (portfolio error)         33.09       14.72        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml      ERROR (portfolio error)         31.96       14.00        None
btor2c-lazyMod.msmie.4.prop1-func-interl.yml           ERROR (portfolio error)        108.85       80.49        None
btor2c-lazyMod.protocols.5.prop1-func-interl.yml       ERROR (portfolio error)         17.91        7.37        None
btor2c-lazyMod.pgm_protocol.4.prop5-func-interl.yml    ERROR (portfolio error)         78.69       50.61        None
btor2c-lazyMod.brp.1.prop1-func-interl.yml             ERROR (portfolio error)         23.21        9.03        None
btor2c-lazyMod.brp2.5.prop3-back-serstep.yml           ERROR (portfolio error)         26.63       10.69        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                           403.05      348.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:             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-19 13:35:35 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-az738-414
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.25 MHz
ram:                     16757.792768 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)            9.46        4.64        None
test15.yml                ERROR (generic error)            9.32        4.53        None
just_assert.yml           true                             5.73        3.27        None
volatile_alias.yml        ERROR (generic error)            6.62        4.09        None
mutex_lock_int.c_1.yml    ERROR (generic error)            9.58        4.67        None
oomInt.yml                true                             7.48        3.78        None
test16.yml                ERROR (generic error)            8.84        4.50        None
mutex_lock_int.yml        ERROR (generic error)            9.18        4.59        None
test18.yml                ERROR (generic error)            9.35        4.52        None
volatile_alias.c_1.yml    ERROR (generic error)            6.68        4.11        None
---------------------------------------------------------------------------------------
Run set 1                 done                            82.24       43.74           -


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-19 13:37:24 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-az585-782
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2820.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.33      105.31        None
loop-crafted/simple_vardep_2.yml                   TIMEOUT                        120.07      108.35        None
nla-digbench-scaling/divbin_valuebound100.yml      TIMEOUT                        120.93      103.39        None
nla-digbench-scaling/mannadiv_valuebound50.yml     ERROR (portfolio error)         21.66       10.06        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    ERROR (portfolio error)         24.47       10.81        None
loops-crafted-1/nested3-1_abstracted.yml           ERROR (portfolio error)         20.16        9.52        None
nla-digbench-scaling/sqrt1-ll_valuebound2.yml      TIMEOUT                        120.79      105.27        None
loop-acceleration/nested_1-2.yml                   TIMEOUT                        120.55      106.59        None
nla-digbench-scaling/hard-ll_valuebound2.yml       ERROR (portfolio error)         27.37       11.22        None
loop-invgen/down.yml                               TIMEOUT                        120.94      106.88        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            94.38      679.84           -


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 (0 / 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-19 13:35:32 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-az1215-985
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2951.257 MHz
ram:                     16757.796864 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.75       89.83        None
recursive-simple/id2_i5_o5-2.yml                                         TIMEOUT                        120.54       75.77        None
recursified_nla-digbench/recursified_geo2-ll.yml                         ERROR (frontend failed)          1.31        0.65        None
recursive/recHanoi03-2.yml                                               TIMEOUT                        120.83       73.57        None
recursified_nla-digbench/recursified_lcm2.yml                            ERROR (frontend failed)          1.37        0.68        None
recursive-simple/id_b3_o2-2.yml                                          TIMEOUT                        120.88       81.36        None
recursified_nla-digbench/recursified_ps3-ll.yml                          ERROR (frontend failed)          1.33        0.65        None
recursive-simple/afterrec-2.yml                                          TIMEOUT                        120.71      111.27        None
recursive-simple/id_i10_o10-2.yml                                        TIMEOUT                        120.49       75.30        None
recursified_loop-crafted/recursified_simple_array_index_value_1-2.yml    ERROR (frontend failed)          1.15        0.59        None
--------------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                                done                             5.89      512.54           -


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)
✅ ReachSafety-Sequentialized (1 / 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-19 13:36: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-az661-425
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3233.393 MHz
ram:                     16757.792768 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                        123.50       43.69        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        TIMEOUT                        120.61       92.84        None
systemc/pipeline.cil-1.yml                                        TIMEOUT                        121.49       52.84        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    TIMEOUT                        120.37       96.50        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            TIMEOUT                        120.27       84.89        None
seq-mthreaded/pals_opt-floodmax.5.ufo.BOUNDED-10.pals.yml         TIMEOUT                        120.68       93.78        None
systemc/toy.cil.yml                                               TIMEOUT                        120.83       61.01        None
seq-mthreaded/pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.yml        TIMEOUT                        120.87       91.79        None
systemc/mem_slave_tlm.5.cil.yml                                   true                            68.85       45.18        None
systemc/token_ring.09.cil-1.yml                                   TIMEOUT                        121.06       45.93        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                            69.93      712.01           -


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:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               9
  Score:                 2 (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-19 13:37:37 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-az1272-519
os:                      Linux-6.2.0-1015-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.566 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.30       93.78        None
Dubois-025.yml             ERROR (portfolio error)         18.67        7.63        None
aim-100-2-0-unsat-4.yml    ERROR (portfolio error)         22.40        8.77        None
AllInterval-014.yml        TIMEOUT                        121.70      104.79        None
AllInterval-005.yml        false(unreach-call)             11.45        4.37        None
aim-100-1-6-unsat-4.yml    ERROR (portfolio error)         22.47        8.80        None
AllInterval-012.yml        TIMEOUT                        121.79      104.98        None
Dubois-100.yml             ERROR (portfolio error)         34.19       12.82        None
AllInterval-009.yml        false(unreach-call)             19.44        9.35        None
aim-200-1-6-unsat-2.yml    ERROR (portfolio error)         30.01       11.33        None
----------------------------------------------------------------------------------------
Run set 1                  done                           158.99      368.37           -


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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@leventeBajczi @mondokz @mondokm