Skip to content

Commit 9ea8830

Browse files
committed
SMTChecker: Add command-line test for Eldarica
1 parent b50d374 commit 9ea8830

File tree

3 files changed

+13
-0
lines changed

3 files changed

+13
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
--model-checker-engine chc --model-checker-solvers eld
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
Warning: CHC: Assertion violation happens here.
2+
--> model_checker_solvers_eld/input.sol:5:3:
3+
|
4+
5 | assert(x > 0);
5+
| ^^^^^^^^^^^^^
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
// SPDX-License-Identifier: GPL-3.0
2+
pragma solidity >=0.0;
3+
contract test {
4+
function f(uint x) public pure {
5+
assert(x > 0);
6+
}
7+
}

0 commit comments

Comments
 (0)