diff --git a/test/cmdlineTests/model_checker_solvers_eld/args b/test/cmdlineTests/model_checker_solvers_eld/args new file mode 100644 index 000000000..e4acd0b46 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_eld/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-solvers eld diff --git a/test/cmdlineTests/model_checker_solvers_eld/err b/test/cmdlineTests/model_checker_solvers_eld/err new file mode 100644 index 000000000..5700a55f3 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_eld/err @@ -0,0 +1 @@ +Warning: CHC analysis was not possible since Eldarica was the only Horn solver enabled, but it was not found in the system. diff --git a/test/cmdlineTests/model_checker_solvers_eld/input.sol b/test/cmdlineTests/model_checker_solvers_eld/input.sol new file mode 100644 index 000000000..7d05ef6e5 --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_eld/input.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_solvers_eld/input.json b/test/cmdlineTests/standard_model_checker_solvers_eld/input.json new file mode 100644 index 000000000..bcf8bd787 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_eld/input.json @@ -0,0 +1,18 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "solvers": ["eld"] + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_solvers_eld/output.json b/test/cmdlineTests/standard_model_checker_solvers_eld/output.json new file mode 100644 index 000000000..05d0edcdd --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_solvers_eld/output.json @@ -0,0 +1,3 @@ +{"errors":[{"component":"general","errorCode":"7267","formattedMessage":"Warning: CHC analysis was not possible since Eldarica was the only Horn solver enabled, but it was not found in the system. + +","message":"CHC analysis was not possible since Eldarica was the only Horn solver enabled, but it was not found in the system.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/libsolidity/smtCheckerTests/eldarica/smoke.sol b/test/libsolidity/smtCheckerTests/eldarica/smoke.sol new file mode 100644 index 000000000..98ab493a0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/eldarica/smoke.sol @@ -0,0 +1,8 @@ +contract C { + function f(uint x) public pure { + assert(x > 0); + } +} +// ==== +// SMTEngine: chc +// SMTSolvers: eld