diff --git a/test/cmdlineTests/standard_model_checker_solvers_none/output.json b/test/cmdlineTests/standard_model_checker_solvers_none/output.json index b237fadce..d5672007e 100644 --- a/test/cmdlineTests/standard_model_checker_solvers_none/output.json +++ b/test/cmdlineTests/standard_model_checker_solvers_none/output.json @@ -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}}} diff --git a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol index c8285a0bc..a98ba962a 100644 --- a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol +++ b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol @@ -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.