[CHC] Add function blocks and check asserts

test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	function f() public {
+		if (x == 0)
+			x = 1;
+	}
+
+	function g() public {
+		if (x == 1)
+			x = 2;
+	}
+
+	function h() public {
+		if (x == 2)
+			x = 0;
+	}
+
+	// This function shows that (x < 9) is not inductive and
+	// a stronger invariant is needed to be found.
+	// (x < 3) is the one found in the end.
+	function j() public {
+		if (x == 7)
+			x = 100;
+	}
+
+	function i() public view {
+		assert(x < 9);
+	}
+}

test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+
+	function f() public {
+		if (x == 0)
+			x = 1;
+	}
+
+	function g() public {
+		if (x == 1)
+			x = 2;
+	}
+
+	function h() public {
+		if (x == 2)
+			x = 0;
+	}
+
+	function j() public {
+		if (x < 2)
+			x = 100;
+	}
+
+	// Fails due to j.
+	function i() public view {
+		assert(x < 2);
+	}
+}
+// ----
+// Warning: (311-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol

@@ -15,6 +15,10 @@ contract C
 		assert(x > 0);
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (136-149): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol

@@ -20,6 +20,10 @@ contract C
 	function f() m n public {
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (170-183): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol

@@ -17,6 +17,10 @@ contract C
 	function f() m public {
 		x = x + 1;
 	}
+
+	function g(uint _x) public {
+		x = _x;
+	}
 }
 // ----
 // Warning: (156-170): Assertion violation happens here