From 429bde9edc53ec38f22ce897287783902e561db1 Mon Sep 17 00:00:00 2001
From: Andrew Gacek <andrew.gacek@gmail.com>
Date: Sat, 16 Feb 2013 21:19:24 -0600
Subject: [PATCH] Include final step in inductive counterexamples

---
 src/jkind/processes/InductiveProcess.java | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/jkind/processes/InductiveProcess.java b/src/jkind/processes/InductiveProcess.java
index 0fb53229e..aa0a28dd5 100644
--- a/src/jkind/processes/InductiveProcess.java
+++ b/src/jkind/processes/InductiveProcess.java
@@ -113,7 +113,7 @@ private void checkProperties(int k) {
 					String p = iterator.next();
 					BoolValue v = (BoolValue) model.getFunctionValue("$" + p, index);
 					if (!v.getBool()) {
-						sendInductiveCounterexample(p, n, k, model);
+						sendInductiveCounterexample(p, n, k+1, model);
 						iterator.remove();
 					}
 				}