Add test from Aon blog post

test/libsolidity/smtCheckerTests/invariants/aon_blog_post.sol

@@ -0,0 +1,47 @@
+pragma experimental SMTChecker;
+contract C {
+	bool a;
+	bool b;
+	bool c;
+	bool d;
+	bool e;
+	bool f;
+	function press_A() public {
+		if(e) { a = true; } else { reset(); }
+	}
+	function press_B() public {
+		if(c) { b = true; } else { reset(); }
+	}
+	function press_C() public {
+		if(a) { c = true; } else { reset(); }
+	}
+	function press_D() public {
+		d = true;
+	}
+	function press_E() public {
+		if(d) { e = true; } else { reset(); }
+	}
+	function press_F() public {
+		if(b) { f = true; } else { reset(); }
+	}
+	function is_not_solved() view public {
+		// f = true can be reached by calling the functions
+		// press_D()
+		// press_E()
+		// press_A()
+		// press_C()
+		// press_B()
+		// press_F()
+		assert(!f);
+	}
+	function reset() internal {
+		a = false;
+		b = false;
+		c = false;
+		d = false;
+		e = false;
+		f = false;
+	}
+}
+// ----
+// Warning 6328: (689-699): Assertion violation happens here