new tests

This commit is contained in:
Leo Alt 2022-05-15 17:46:02 +02:00
parent d70d137898
commit d8ebc29c55
6 changed files with 38 additions and 0 deletions

View File

@ -0,0 +1 @@
--model-checker-engine chc --model-checker-solvers eld

View File

@ -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.

View File

@ -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);
}
}

View File

@ -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"]
}
}
}

View File

@ -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}}}

View File

@ -0,0 +1,8 @@
contract C {
function f(uint x) public pure {
assert(x > 0);
}
}
// ====
// SMTEngine: chc
// SMTSolvers: eld