diff --git a/main.go b/main.go
index 65438bc..45012f2 100644
--- a/main.go
+++ b/main.go
@@ -190,7 +190,7 @@ func generateBenchmarkStateful() error {
 		if depth < 1 {
 			indentStr := strings.Repeat("  ", indent)
 			return fmt.Sprintf(
-				`%vemit AssertionFailed("%v"); assert(false);  // bug`,
+				`%vfound[%v] = true; return -1;  // bug`,
 				indentStr,
 				rv,
 			)
@@ -240,6 +240,19 @@ func generateBenchmarkStateful() error {
 	}
 	bodyStr := bodyBuilder.String()
 
+	var invBuilder strings.Builder
+	for i := 1; i < retCnt; i++ {
+		_, _ = fmt.Fprintf(
+			&invBuilder,
+			`  function invariant_%v() external { if (m.found(%v)) { fail("%v"); } }
+`,
+			i,
+			i,
+			i,
+		)
+	}
+	invStr := invBuilder.String()
+
 	type ProgramPlaceholders struct {
 		ParamsStr string
 		ArgsStr   string
@@ -247,6 +260,7 @@ func generateBenchmarkStateful() error {
 		DimY      int
 		BodyStr   string
 		RetCnt    int
+		InvStr    string
 	}
 	placeholders := ProgramPlaceholders{
 		ParamsStr: paramsStr,
@@ -255,6 +269,7 @@ func generateBenchmarkStateful() error {
 		DimY:      dimY,
 		BodyStr:   bodyStr,
 		RetCnt:    retCnt,
+		InvStr:    invStr,
 	}
 	progTemplate := `pragma solidity ^0.8.19;
 /// automatically generated by Daedaluzz
@@ -262,36 +277,48 @@ contract Maze {
   event AssertionFailed(string message);
   uint64 private x;
   uint64 private y;
+  mapping (uint64 => bool) public found;
   function moveNorth({{.ParamsStr}}) payable external returns (int64) {
     uint64 ny = y + 1;
     require(ny < {{.DimY}});
-    y = ny;
-    return step({{.ArgsStr}});
+    int64 r = step(x, ny, {{.ArgsStr}});
+    if (0 <= r) { y = ny; }
+    return r;
   }
   function moveSouth({{.ParamsStr}}) payable external returns (int64) {
     require(0 < y);
     uint64 ny = y - 1;
-    y = ny;
-    return step({{.ArgsStr}});
+    int64 r = step(x, ny, {{.ArgsStr}});
+    if (0 <= r) { y = ny; }
+    return r;
   }
   function moveEast({{.ParamsStr}}) payable external returns (int64) {
     uint64 nx = x + 1;
     require(nx < {{.DimX}});
-    x = nx;
-    return step({{.ArgsStr}});
+    int64 r = step(nx, y, {{.ArgsStr}});
+    if (0 <= r) { x = nx; }
+    return r;
   }
   function moveWest({{.ParamsStr}}) payable external returns (int64) {
     require(0 < x);
     uint64 nx = x - 1;
-    x = nx;
-    return step({{.ArgsStr}});
+    int64 r = step(nx, y, {{.ArgsStr}});
+    if (0 <= r) { x = nx; }
+    return r;
   }
-  function step({{.ParamsStr}}) internal returns (int64) {
+  function step(uint64 x, uint64 y, {{.ParamsStr}}) internal returns (int64) {
     unchecked {
 {{.BodyStr}}      return {{.RetCnt}};
     }
   }
 }
+import "forge-std/Test.sol";
+contract TestMaze is Test {
+  Maze m;
+  function setUp() external {
+    m = new Maze();
+  }
+{{.InvStr}}}
 `
 	parsedTemplate, parseErr := template.New("program").Parse(progTemplate)
 	if parseErr != nil {