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

SMTLIB integration fixes #271

Merged

mondokm merged 15 commits into master from smtlib-fixes

Jun 25, 2024

Contributor

mondokm commented Jun 24, 2024

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

cvc5: A dummy assertion is added to formula A in case of interpolation.
princess: The HashMap is replaced with IdentityHashMap, similarly to SmtInterpol (Fix smtinterpol interpolation (#253) #261).
Support for latest versions of cvc5, Z3 and princess.

mondokm and others added 15 commits

June 20, 2024 14:10


          Fixed Windows filename for cvc5

715fadf


          Add dummy assertion to formula A for interpolation in cvc5

47b796c


          Add support for cvc5 1.1.1 and 1.1.2

978ab04


          Fixed a typo in an SMTInterpol url

169495d


          Reformatted code

213ce46


          Fixed Windows filename for cvc5

b253b5a


          Add dummy assertion to formula A for interpolation in cvc5


          Add support for cvc5 1.1.1 and 1.1.2

bd09d19


          Fixed a typo in an SMTInterpol url

1d8c8d5


          Reformatted code

a689368


          Merge remote-tracking branch 'origin/smtlib-fixes' into smtlib-fixes

c41f3ba


          Add new z3 versions

533a540


          Add new princess version

a0d7355


          Fix princess interpolation issue

d956072


          Bump version

b5b2792

github-actions bot commented Jun 24, 2024

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

✅ ConcurrencySafety-Main (3 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:12 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az570-320
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3182.976 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ConcurrencySafety-Main
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      11.01        5.03        None
pthread-atomic/read_write_lock-1.yml          true                            11.25        4.24        None
pthread-wmm/rfi003_tso.yml                    TIMEOUT                        120.60       90.18        None
pthread/lazy01.yml                            false(unreach-call)              7.54        3.23        None
pthread-wmm/mix000.oepc.yml                   false(unreach-call)             19.94        7.56        None
-----------------------------------------------------------------------------------------------------------
Run set 1                                     done                            49.83      110.96           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               3
    correct true:        1
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                 4 (max: 8)

✅ ConcurrencySafety-MemSafety (4 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:08 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1108-192
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3022.179 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety
Run set 4 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      11.02        5.23        None
pthread-atomic/read_write_lock-1.yml          true                             9.47        3.73        None
pthread-wmm/rfi003_tso.yml                    true                            15.35        6.18        None
pthread/lazy01.yml                            true                             7.38        3.15        None
pthread-wmm/mix000.oepc.yml                   true                            13.74        5.62        None
-----------------------------------------------------------------------------------------------------------
Run set 4                                     done                            56.94       24.44           -

Statistics:              5 Files
  correct:               4
    correct true:        4
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 8 (max: 10)

✅ ConcurrencySafety-NoOverflows (4 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:03 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1113-373
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.352 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows
Run set 3 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      11.69        5.33        None
pthread-atomic/read_write_lock-1.yml          true                             8.79        3.48        None
pthread-wmm/rfi003_tso.yml                    true                            16.52        6.57        None
pthread/lazy01.yml                            true                             7.85        3.29        None
pthread-wmm/mix000.oepc.yml                   true                            14.95        6.17        None
-----------------------------------------------------------------------------------------------------------
Run set 3                                     done                            59.77       25.37           -


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

Statistics:              5 Files
  correct:               4
    correct true:        4
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 8 (max: 10)

✅ NoDataRace-Main (4 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:15 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1499-511
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3129.272 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race.NoDataRace-Main
Run set 2 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      10.97        5.20        None
pthread-atomic/read_write_lock-1.yml          true                            11.46        4.33        None
pthread-wmm/rfi003_tso.yml                    true                            18.00        7.08        None
pthread/lazy01.yml                            true                             7.30        3.12        None
pthread-wmm/mix000.oepc.yml                   true                            17.70        6.97        None
-----------------------------------------------------------------------------------------------------------
Run set 2                                     done                            65.39       27.23           -


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               4
    correct true:        4
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 8 (max: 10)

✅ ReachSafety-Arrays (1 / 0 / 5)

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:                    Mon, 2024-06-24 13:28:33 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1113-373
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3238.293 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Arrays
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                         status                       cpu time   wall time        host
---------------------------------------------------------------------------------------------------------------
array-examples/standard_partition_ground-2.yml    TIMEOUT                         76.16      161.00        None
array-crafted/mapavg4.yml                         TIMEOUT                         77.18      161.02        None
array-programs/copysome2-1.yml                    TIMEOUT                         77.92      161.02        None
array-examples/sanfoundry_24-1.yml                true                            11.84      103.26        None
array-multidimensional/max-2-u.yml                ERROR (frontend failed)          1.76        0.73        None
---------------------------------------------------------------------------------------------------------------
Run set 1                                         done                            13.95      588.27           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 10)

✅ ReachSafety-BitVectors (3 / 0 / 5)

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:                    Mon, 2024-06-24 13:27:31 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1456-774
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.209 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-BitVectors
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                      status                       cpu time   wall time        host
------------------------------------------------------------------------------------------------------------
bitvector/gcd_4.yml                            true                             6.65        2.90        None
bitvector/soft_float_1-3a.c.cil.yml            false(unreach-call)             31.82       17.17        None
bitvector-regression/integerpromotion-3.yml    false(unreach-call)              5.02        2.54        None
bitvector/sum02-1.yml                          Parsing OK                      36.49       18.39        None
bitvector-loops/diamond_2-1.yml                TIMEOUT                        121.74       86.02        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                            74.65      127.64           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               3
    correct true:        1
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                 4 (max: 6)

❓ ReachSafety-Combinations (0 / 0 / 5)

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:                    Mon, 2024-06-24 13:32:10 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1247-446
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3216.874 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Combinations
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                                status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------------------------
pc_sfifo_3.cil+token_ring.02.cil-2.yml                   TIMEOUT                        120.38       74.60        None
Problem05_label47+token_ring.02.cil-1.yml                TIMEOUT                        120.34       95.11        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                   TIMEOUT                        120.15      107.63        None
Problem05_label45+token_ring.01.cil-2.yml                TIMEOUT                        120.58       92.16        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml    TIMEOUT                        120.96       69.77        None
----------------------------------------------------------------------------------------------------------------------
Run set 1                                                done                             0.59      440.81           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 5)

✅ ReachSafety-ControlFlow (1 / 0 / 5)

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:                    Mon, 2024-06-24 13:27:39 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az840-896
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2694.23 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-ControlFlow
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                              status                       cpu time   wall time        host
--------------------------------------------------------------------------------------------------------------------
longjmp/68-longjmp_18-simple-else_unknown_1_pos.yml    ERROR (frontend failed)          3.77        1.34        None
locks/test_locks_11.yml                                TIMEOUT                        122.64      102.80        None
locks/test_locks_5.yml                                 true                            13.73        5.34        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml    ERROR (frontend failed)          4.30        1.53        None
longjmp/68-longjmp_11-counting-return_true.yml         ERROR (frontend failed)          2.09        0.85        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                            23.35      112.50           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 8)

❓ ReachSafety-ECA (0 / 0 / 5)

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:                    Mon, 2024-06-24 13:35:19 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az698-74
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3240.134 MHz
ram:                     16757.338112 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-ECA
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                              status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------
eca-rers2012/Problem06_label18.yml     TIMEOUT                        122.07       79.22        None
eca-rers2012/Problem06_label11.yml     TIMEOUT                        121.02       76.15        None
eca-programs/Problem101_label07.yml    TIMEOUT                        121.27       71.89        None
eca-rers2012/Problem05_label44.yml     TIMEOUT                        120.43       72.50        None
eca-rers2012/Problem04_label05.yml     TIMEOUT                        121.02       73.07        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             0.60      375.76           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 7)

✅ ReachSafety-Floats (4 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:16 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1778-473
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3279.904 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Floats
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                          status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------------------
float-benchs/float_double.yml                      true                             5.43        2.82        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    TIMEOUT                        120.42      113.11        None
float-benchs/float_int_inv_square.yml              false(unreach-call)              6.02        3.00        None
floats-cdfpl/square_3.yml                          false(unreach-call)             75.68       71.51        None
floats-cbmc-regression/float11.yml                 true                             5.26        2.76        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            92.40      194.22           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               4
    correct true:        2
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 6 (max: 8)

❓ ReachSafety-Hardware (0 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:47 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az736-148
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3244.475 MHz
ram:                     16757.334016 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Hardware
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                            status                       cpu time   wall time        host
------------------------------------------------------------------------------------------------------------------
btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml      TIMEOUT                        120.60      111.71        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml    TIMEOUT                        120.42       99.25        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml    TIMEOUT                        120.38       95.87        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml           TIMEOUT                        123.11       94.63        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml    TIMEOUT                        120.67       86.80        None
------------------------------------------------------------------------------------------------------------------
Run set 1                                            done                             0.59      490.88           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 9)

✅ ReachSafety-Heap (5 / 0 / 5)

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:                    Mon, 2024-06-24 13:28:01 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az575-755
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.175 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Heap
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                 status                       cpu time   wall time        host
---------------------------------------------------------------------------------------
test09.yml                true                             9.89        4.71        None
test15.yml                true                             8.76        4.28        None
just_assert.yml           true                             5.45        2.58        None
volatile_alias.yml        true                             8.01        4.18        None
mutex_lock_int.c_1.yml    true                             8.97        4.37        None
---------------------------------------------------------------------------------------
Run set 1                 done                            41.06       20.64           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               5
    correct true:        5
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               0
  Score:                10 (max: 10)

✅ ReachSafety-Loops (1 / 0 / 5)

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:                    Mon, 2024-06-24 13:30:01 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1766-97
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2871.636 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Loops
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                          status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------------------
nla-digbench/ps3-ll.yml                            TIMEOUT                        120.40      107.17        None
loop-crafted/simple_vardep_2.yml                   TIMEOUT                        120.91      109.61        None
nla-digbench-scaling/divbin_valuebound100.yml      TIMEOUT                        120.68      107.28        None
nla-digbench-scaling/mannadiv_valuebound50.yml     true                            22.96       10.34        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    Parsing OK                      28.98       12.38        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            52.18      347.60           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 9)

✅ ReachSafety-Recursive (1 / 0 / 5)

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:                    Mon, 2024-06-24 13:27:51 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az693-187
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3203.96 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Recursive
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                           status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------------
recursive-simple/id_o100.yml                        Parsing OK                      18.26        7.31        None
recursive-simple/id2_i5_o5-2.yml                    true                            14.29        5.33        None
recursified_nla-digbench/recursified_geo2-ll.yml    TIMEOUT                         35.51      161.02        None
recursive/recHanoi03-2.yml                          TIMEOUT                        120.37       90.21        None
recursified_nla-digbench/recursified_lcm2.yml       TIMEOUT                        120.38      113.78        None
-----------------------------------------------------------------------------------------------------------------
Run set 1                                           done                            32.88      379.02           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 9)

✅ ReachSafety-Sequentialized (1 / 0 / 5)

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:                    Mon, 2024-06-24 13:29:14 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az914-840
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2595.373 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Sequentialized
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                                         status                       cpu time   wall time        host
-------------------------------------------------------------------------------------------------------------------------------
systemc/transmitter.12.cil.yml                                    TIMEOUT                        121.04      109.73        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        TIMEOUT                        120.36       94.14        None
systemc/pipeline.cil-1.yml                                        TIMEOUT                        120.37      105.61        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    TIMEOUT                        120.66       94.37        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            false(unreach-call)            104.26       66.80        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                           103.02      471.69           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               1
    correct true:        0
    correct false:       1
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 1 (max: 6)

❓ ReachSafety-XCSP (0 / 0 / 5)

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:                    Mon, 2024-06-24 13:27:36 UTC
tool:                    Theta 5.2.1
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az738-293
os:                      Linux-6.5.0-1022-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3222.521 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-XCSP
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                  status                       cpu time   wall time        host
----------------------------------------------------------------------------------------
CostasArray-14.yml         TIMEOUT                        120.17      105.62        None
Dubois-025.yml             TIMEOUT                        120.30      106.39        None
aim-100-2-0-unsat-4.yml    TIMEOUT                        120.17      107.42        None
AllInterval-014.yml        TIMEOUT                        120.43      105.14        None
AllInterval-005.yml        TIMEOUT                        120.30      105.07        None
----------------------------------------------------------------------------------------
Run set 1                  done                             0.61      530.66           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


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

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 7)

mondokm merged commit 928c853 into master

83 of 84 checks passed

mondokm deleted the smtlib-fixes branch

June 25, 2024 07:37

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet