From 9ea88304f2658cbe771dc7ce29dfc15e98d3d604 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Tue, 5 Mar 2024 20:13:32 +0100 Subject: [PATCH] SMTChecker: Add command-line test for Eldarica --- test/cmdlineTests/model_checker_solvers_eld/args | 1 + test/cmdlineTests/model_checker_solvers_eld/err | 5 +++++ test/cmdlineTests/model_checker_solvers_eld/input.sol | 7 +++++++ 3 files changed, 13 insertions(+) create mode 100644 test/cmdlineTests/model_checker_solvers_eld/args create mode 100644 test/cmdlineTests/model_checker_solvers_eld/err create mode 100644 test/cmdlineTests/model_checker_solvers_eld/input.sol diff --git a/test/cmdlineTests/model_checker_solvers_eld/args b/test/cmdlineTests/model_checker_solvers_eld/args new file mode 100644 index 000000000000..e4acd0b46b71 --- /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 000000000000..ff7ad37b313e --- /dev/null +++ b/test/cmdlineTests/model_checker_solvers_eld/err @@ -0,0 +1,5 @@ +Warning: CHC: Assertion violation happens here. + --> model_checker_solvers_eld/input.sol:5:3: + | +5 | assert(x > 0); + | ^^^^^^^^^^^^^ 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 000000000000..7d05ef6e5f3e --- /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