cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

update tests

Browse Source
This commit is contained in:
Leo Alt 2022-05-10 19:25:27 +02:00
parent 93f9638a1b
commit cbaba6f913
2 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/cmdlineTests/standard_model_checker_solvers_none/output.json
View File

@ -1,5 +1,5 @@
{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was enabled.
{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was found and enabled.
","message":"CHC analysis was not possible since no Horn solver was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled.
","message":"CHC analysis was not possible since no Horn solver was found and enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled.
","message":"BMC analysis was not possible since no SMT solver was found and enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol
View File

@ -21,4 +21,6 @@ contract C is B {
// Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here.
// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
// Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here.
// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
// Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here.
// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.