SMTChecker: Add command-line test for cvc4

ethereum · May 8, 2024 · 06f5be1 · 06f5be1
1 parent b4341d2
commit 06f5be1
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 0 deletions.
diff --git a/test/cmdlineTests/model_checker_cvc4/args b/test/cmdlineTests/model_checker_cvc4/args
@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-solvers cvc4
diff --git a/test/cmdlineTests/model_checker_cvc4/err b/test/cmdlineTests/model_checker_cvc4/err
@@ -0,0 +1,10 @@
+Warning: BMC: Assertion violation happens here.
+ --> test/cmdlineTests/model_checker_cvc4/input.sol:5:3:
+  |
+5 | 		assert(x > 0);
+  | 		^^^^^^^^^^^^^
+Note: Counterexample:
+  x = 0
+
+Note: Callstack:
+Note:
diff --git a/test/cmdlineTests/model_checker_cvc4/input.sol b/test/cmdlineTests/model_checker_cvc4/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);
+	}
+}
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		--model-checker-engine bmc --model-checker-solvers cvc4