k-induction and bmc send 'unknown' after max-iterations

loonwerks · Apr 18, 2015 · 1ad2c6e · 1ad2c6e
1 parent 7316827
commit 1ad2c6e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/jkind/src/jkind/engines/BmcEngine.java b/jkind/src/jkind/engines/BmcEngine.java
@@ -33,13 +33,14 @@ public void main() {
 			comment("K = " + (k + 1));
 			processMessages();
 			if (properties.isEmpty()) {
-				break;
+				return;
 			}
 			createVariables(k);
 			assertBaseTransition(k);
 			checkProperties(k);
 			assertProperties(k);
 		}
+		sendUnknown(properties);
 	}
 
 	private void checkProperties(int k) {

diff --git a/jkind/src/jkind/engines/KInductionEngine.java b/jkind/src/jkind/engines/KInductionEngine.java
@@ -48,9 +48,10 @@ public void main() {
 			assertTransitionAndInvariants(kCurrent);
 			checkProperties(kCurrent);
 			if (properties.isEmpty()) {
-				break;
+				return;
 			}
 		}
+		sendUnknown(properties);
 	}
 
 	private void processMessagesAndWait() {