aboutsummaryrefslogtreecommitdiffstats
path: root/test/libsolidity/smtCheckerTestsJSON/simple.sol
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-11-15 23:47:52 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2018-11-23 18:51:06 +0800
commit0ff4cbe51ba653397a1937c8c08b3d09541492ef (patch)
tree03a8798bca8f2ef221d77fc8a4c6c5390105800c /test/libsolidity/smtCheckerTestsJSON/simple.sol
parent6251a289dd55cc54f8da5a907dc4982a4b5e57fa (diff)
downloaddexon-solidity-0ff4cbe51ba653397a1937c8c08b3d09541492ef.tar.gz
dexon-solidity-0ff4cbe51ba653397a1937c8c08b3d09541492ef.tar.zst
dexon-solidity-0ff4cbe51ba653397a1937c8c08b3d09541492ef.zip
Add SMTChecker tests for standard JSON
Diffstat (limited to 'test/libsolidity/smtCheckerTestsJSON/simple.sol')
-rw-r--r--test/libsolidity/smtCheckerTestsJSON/simple.sol10
1 files changed, 10 insertions, 0 deletions
diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.sol b/test/libsolidity/smtCheckerTestsJSON/simple.sol
new file mode 100644
index 00000000..6bc7193d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/simple.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+ function f(uint x) public pure {
+ assert(x > 0);
+ }
+}
+// ----
+// Warning: (82-95): Assertion violation happens here