-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ b1b345e 🚀
- Loading branch information
0 parents
commit 0281bc4
Showing
49,434 changed files
with
10,094,519 additions
and
0 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| theta.mit.bme.hu |
22 changes: 22 additions & 0 deletions
22
...n-BOUNDED/theta.2.2024-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.08_rand_cas.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/pthread-ext/08_rand_cas.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/pthread-ext/08_rand_cas.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/pthread-ext/08_rand_cas.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [NONLIN_INT] | ||
| Frontend finished: (in 1119 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 2 -> [1, 0] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...theta.2.2024-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.11_fmaxsymopt-pthread.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/pthread-ext/11_fmaxsymopt-pthread.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/pthread-ext/11_fmaxsymopt-pthread.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/pthread-ext/11_fmaxsymopt-pthread.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [NONLIN_INT, ARR] | ||
| Frontend finished: (in 956 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...-45-23.logfiles/SV-COMP24_unreach-call.13-privatized_18-first-reads_unknown_1_neg.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/goblint-regression/13-privatized_18-first-reads_unknown_1_neg.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/goblint-regression/13-privatized_18-first-reads_unknown_1_neg.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/goblint-regression/13-privatized_18-first-reads_unknown_1_neg.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 820 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
....logfiles/SV-COMP24_unreach-call.13-privatized_19-publish-precision_unknown_2_pos.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 907 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...-45-23.logfiles/SV-COMP24_unreach-call.13-privatized_31-traces-mine-vs-mutex_true.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/goblint-regression/13-privatized_31-traces-mine-vs-mutex_true.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 907 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.13-privatized_37-traces-ex-4_true.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/goblint-regression/13-privatized_37-traces-ex-4_true.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/goblint-regression/13-privatized_37-traces-ex-4_true.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/goblint-regression/13-privatized_37-traces-ex-4_true.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 741 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...-45-23.logfiles/SV-COMP24_unreach-call.13-privatized_41-traces-ex-7_unknown_1_pos.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/goblint-regression/13-privatized_41-traces-ex-7_unknown_1_pos.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 911 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...n-BOUNDED/theta.2.2024-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.14_spin2003.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/pthread-ext/14_spin2003.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/pthread-ext/14_spin2003.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/pthread-ext/14_spin2003.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 644 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
....2.2024-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.18_read_write_lock-pthread.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/pthread-ext/18_read_write_lock-pthread.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/pthread-ext/18_read_write_lock-pthread.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/pthread-ext/18_read_write_lock-pthread.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 662 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
...4-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.28-race_reach_46-escape_racefree.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/goblint-regression/28-race_reach_46-escape_racefree.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/goblint-regression/28-race_reach_46-escape_racefree.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/goblint-regression/28-race_reach_46-escape_racefree.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 934 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 1 -> [0] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
22 changes: 22 additions & 0 deletions
22
....2.2024-08-29_16-45-23.logfiles/SV-COMP24_unreach-call.31_simple_loop5_vs-pthread.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| Theta/theta-start.sh sv-benchmarks/c/pthread-ext/31_simple_loop5_vs-pthread.i --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/Theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/Theta/theta.jar --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --loglevel INFO --property sv-benchmarks/c/properties/unreach-call.prp --architecture ILP32 --portfolio BOUNDED --input sv-benchmarks/c/pthread-ext/31_simple_loop5_vs-pthread.i --smt-home /home/runner/work/theta/theta/Theta/solvers | ||
| Registered Legacy-Z3 SolverManager | ||
| Registered Z3 SolverManager | ||
| Registered JavaSMT SolverManager | ||
| Registered SMT-LIB SolverManager | ||
| Parsing the input sv-benchmarks/c/pthread-ext/31_simple_loop5_vs-pthread.i as C | ||
| WARNING: signedness of the type char is implementation specific. Right now it is interpreted as a signed char. | ||
| WARNING: CompoundDefinitions are not yet implemented! | ||
| WARNING: Unknown simple type union pthread_attr_t | ||
| WARNING: enums are not yet supported! Using int instead. | ||
| Arithmetic: [] | ||
| Frontend finished: (in 811 ms) | ||
| ParsingResult Success | ||
| Alias graph size: 0 -> [] | ||
| Starting verification of UnnamedXcfa using PORTFOLIO | ||
| Process failed! (hu.bme.mit.theta.xcfa.cli.portfolio.BoundedKt.boundedPortfolio(bounded.kt:78), java.lang.UnsupportedOperationException: Multithreading for bounded checkers not supported) |
Oops, something went wrong.