Skip to content

Commit

Permalink
SMTChecker: Add command-line test for invariants from Eldarica
Browse files Browse the repository at this point in the history
  • Loading branch information
blishko committed Apr 23, 2024
1 parent 484ee37 commit 5df3915
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 0 deletions.
@@ -0,0 +1 @@
--model-checker-engine chc --model-checker-invariants contract --model-checker-solvers eld
4 changes: 4 additions & 0 deletions test/cmdlineTests/model_checker_invariants_contract_eld/err
@@ -0,0 +1,4 @@
Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

Info: Contract invariant(s) for model_checker_invariants_contract_eld/input.sol:test:
(x = 0)
@@ -0,0 +1,8 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
uint x;
function f() public view {
assert(x < 10);
}
}

0 comments on commit 5df3915

Please sign in to comment.