aboutsummaryrefslogtreecommitdiffstats
path: root/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol
diff options
context:
space:
mode:
Diffstat (limited to 'test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol')
-rw-r--r--test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol9
1 files changed, 9 insertions, 0 deletions
diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol
new file mode 100644
index 00000000..b9fae4ee
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+ function f(uint x) public pure {
+ if (x >= 0) { revert(); }
+ }
+}
+// ----
+// Warning: (94-100): Condition is always true.
+// Warning: (104-112): Assertion checker does not yet implement this type of function call.