From d617ef461e9e0648a74b07d0636541ea044f9db8 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 31 Mar 2021 17:11:44 +0200
Subject: [PATCH] Add new tests

---
 test/libsolidity/smtCheckerTests/options/engine_none.sol | 7 +++++++
 test/libsolidity/smtCheckerTests/options/pragma.sol      | 9 +++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/options/engine_none.sol
 create mode 100644 test/libsolidity/smtCheckerTests/options/pragma.sol

diff --git a/test/libsolidity/smtCheckerTests/options/engine_none.sol b/test/libsolidity/smtCheckerTests/options/engine_none.sol
new file mode 100644
index 000000000..f14eb43f3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/options/engine_none.sol
@@ -0,0 +1,7 @@
+contract C {
+    function f(uint x) public pure {
+        assert(x > 0);
+    }
+}
+// ====
+// SMTEngine: none
diff --git a/test/libsolidity/smtCheckerTests/options/pragma.sol b/test/libsolidity/smtCheckerTests/options/pragma.sol
new file mode 100644
index 000000000..b3e35ee02
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/options/pragma.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+    function f(uint x) public pure {
+        assert(x > 0);
+    }
+}
+// ----
+// Warning 5523: (0-31): The SMTChecker pragma has been deprecated and will be removed in the future. Please use the "model checker engine" compiler setting to activate the SMTChecker instead. If the pragma is enabled, all engines will be used.
+// Warning 6328: (90-103): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)