From 4d414a6d58d5a3d16655fcc27d51aeb283fc51dc Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Fri, 27 Aug 2021 11:40:33 +0200 Subject: [PATCH] Update commandline tests --- .../model_checker_solvers_smtlib2/err | 4 ++ .../output.json | 40 ------------------- .../output.json | 8 +++- 3 files changed, 10 insertions(+), 42 deletions(-) diff --git a/test/cmdlineTests/model_checker_solvers_smtlib2/err b/test/cmdlineTests/model_checker_solvers_smtlib2/err index 9a156ff90..3aa989348 100644 --- a/test/cmdlineTests/model_checker_solvers_smtlib2/err +++ b/test/cmdlineTests/model_checker_solvers_smtlib2/err @@ -1,3 +1,7 @@ +Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. +Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. diff --git a/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json b/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json index 2f260231c..955b97025 100644 --- a/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json +++ b/test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json @@ -41,46 +41,6 @@ A.constructor() A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. Counterexample: -y = 0 - -Transaction trace: -A.constructor() -B.g(0) - --> Source:5:7: - | -5 | \t\t\t\t\t\tassert(y > 0); - | \t\t\t\t\t\t^^^^^^^^^^^^^ - -","message":"CHC: Assertion violation happens here. -Counterexample: - -y = 0 - -Transaction trace: -A.constructor() -B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. -Counterexample: - -x = 0 - -Transaction trace: -A.constructor() -A.f(0) - --> Source:10:7: - | -10 | \t\t\t\t\t\tassert(x > 0); - | \t\t\t\t\t\t^^^^^^^^^^^^^ - -","message":"CHC: Assertion violation happens here. -Counterexample: - -x = 0 - -Transaction trace: -A.constructor() -A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here. -Counterexample: - z = 0 Transaction trace: diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json index 3b41e64ca..866727f4b 100644 --- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json +++ b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json @@ -145,8 +145,12 @@ (assert (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int)) (=> error_target_3_0 false))) -(check-sat)"}},"errors":[{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. +(check-sat)"}},"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. -","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. + +","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + +","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. ","message":"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}