diff --git a/jkind/src/jkind/processes/InductiveProcess.java b/jkind/src/jkind/processes/InductiveProcess.java
index df14d9887..5c1a78db4 100644
--- a/jkind/src/jkind/processes/InductiveProcess.java
+++ b/jkind/src/jkind/processes/InductiveProcess.java
@@ -116,8 +116,8 @@ private void checkProperties(int k) {
 		while (!possiblyValid.isEmpty()) {
 			Result result = solver.query(getInductiveQuery(k, possiblyValid));
 
-			if (result instanceof SatResult) {
-				Model model = ((SatResult) result).getModel();
+			if (result instanceof SatResult || result instanceof UnknownResult) {
+				Model model = getModel(result);
 				Iterator<String> iterator = possiblyValid.iterator();
 				while (iterator.hasNext()) {
 					String p = iterator.next();
@@ -133,15 +133,20 @@ private void checkProperties(int k) {
 				addPropertiesAsInvariants(k, possiblyValid);
 				sendValid(possiblyValid, k);
 				return;
-			} else if (result instanceof UnknownResult) {
-				properties.removeAll(possiblyValid);
-				// We report nothing in hopes that the base process at least
-				// finds a counterexample
-				return;
 			}
 		}
 	}
 
+	private Model getModel(Result result) {
+		if (result instanceof SatResult) {
+			return ((SatResult) result).getModel();
+		} else if (result instanceof UnknownResult) {
+			return ((UnknownResult) result).getModel();
+		} else {
+			throw new IllegalArgumentException();
+		}
+	}
+
 	private void addPropertiesAsInvariants(int k, List<String> valid) {
 		List<Invariant> propertiesAsInvariants = new ArrayList<>();
 		for (String property : valid) {
diff --git a/jkind/src/jkind/solvers/UnknownResult.java b/jkind/src/jkind/solvers/UnknownResult.java
index 6fd50281a..15bafa328 100644
--- a/jkind/src/jkind/solvers/UnknownResult.java
+++ b/jkind/src/jkind/solvers/UnknownResult.java
@@ -1,5 +1,14 @@
 package jkind.solvers;
 
 public class UnknownResult extends Result {
+	final private Model model;
 
+	public UnknownResult(Model model) {
+		super();
+		this.model = model;
+	}
+
+	public Model getModel() {
+		return model;
+	}
 }
diff --git a/jkind/src/jkind/solvers/z3/Z3Solver.java b/jkind/src/jkind/solvers/z3/Z3Solver.java
index 6424923c8..acaf9675b 100644
--- a/jkind/src/jkind/solvers/z3/Z3Solver.java
+++ b/jkind/src/jkind/solvers/z3/Z3Solver.java
@@ -50,7 +50,10 @@ public Result query(Sexp sexp) {
 		} else if (isUnsat(status)) {
 			result = new UnsatResult();
 		} else {
-			result = new UnknownResult();
+			// Even for unknown we can get a partial model
+			send("(get-model)");
+			send("(echo \"" + DONE + "\")");
+			result = new UnknownResult(parseModel(readFromSolver()));
 		}
 
 		return result;