4 files changed, 43 insertions, 0 deletions
diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json
new file mode 100644
index 00000000..2ed5150d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/multi.json
@@ -0,0 +1,11 @@
+{
+  "auxiliaryInput":
+  {
+	  "smtlib2responses":
+	  {
+		  "0x0426cd198d1e7123a28ffac2b759a666b86508ad046babf5166500dd6d8ed308": "unsat\n(error \"line 31 column 26: model is not available\")",
+		  "0xa51ca41ae407f5a727f27101cbc079834743cc8955f9f585582034ca634953f6": "sat\n((|EVALEXPR_0| 1))",
+		  "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
+	  }
+  }
+}
diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.sol b/test/libsolidity/smtCheckerTestsJSON/multi.sol
new file mode 100644
index 00000000..e0d69b1d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/multi.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		assert(x > 0);
+		assert(x > 100);
+		assert(x >= 0);
+	}
+}
+// ----
+// Warning: (82-95): Assertion violation happens here
+// Warning: (99-114): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json
new file mode 100644
index 00000000..fd976b63
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/simple.json
@@ -0,0 +1,9 @@
+{
+  "auxiliaryInput":
+  {
+	  "smtlib2responses":
+	  {
+		  "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
+	  }
+  }
+}
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