aboutsummaryrefslogtreecommitdiffstats
path: root/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol
diff options
context:
space:
mode:
Diffstat (limited to 'test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol')
-rw-r--r--test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol6
1 files changed, 6 insertions, 0 deletions
diff --git a/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol b/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol
new file mode 100644
index 00000000..8bd6e61a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol
@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+contract C {
+ function f(uint a) public pure { assert(a == 2); }
+}
+// ----
+// Warning: (82-96): Assertion violation happens here