Bug fix: Handle 'unknown' SMT results during invariant generation

This fixes a bug reported by Anthony Aiello and Aaron Fifarek. When
the invariant generator received an 'unknown' result it was treating
it like an 'unsat' result. This caused properties to be erroneously
reported as true.

This bug only appeared in the inductive step part of the invariant
generation. Handling of 'unknown' in the base step was fixed in
99394a8 to address issue #20. This
looks like a case that slipped through at that time.

jkind/src/jkind/engines/invariant/AbstractInvariantGenerationEngine.java

@@ -21,8 +21,7 @@
 import jkind.solvers.Model;
 import jkind.solvers.ModelEvaluator;
 import jkind.solvers.Result;
-import jkind.solvers.SatResult;
-import jkind.solvers.UnknownResult;
+import jkind.solvers.UnsatResult;
 import jkind.translation.Specification;
 import jkind.util.SexpUtil;
 
@@ -77,14 +76,16 @@ private void refineBaseStep(int k, StructuredInvariant invariant) {
 			Sexp query = SexpUtil.conjoinInvariants(invariant.toExprs(), k);
 			result = solver.query(query);
 
-			if (result instanceof SatResult) {
-				Model model = ((SatResult) result).getModel();
+			if (!(result instanceof UnsatResult)) {
+				Model model = getModel(result);
+				if (model == null) {
+					comment("No model - unable to continue");
+					throw new StopException();
+				}
 				invariant.refine(new ModelEvaluator(model, k));
 				comment("Finished single base step refinement");
-			} else if (result instanceof UnknownResult) {
-				throw new StopException();
 			}
-		} while (!invariant.isTrivial() && result instanceof SatResult);
+		} while (!invariant.isTrivial() && !(result instanceof UnsatResult));
 
 		solver.pop();
 	}
@@ -104,12 +105,16 @@ private void refineInductiveStep(int k, StructuredInvariant original) {
 
 			result = solver.query(getInductiveQuery(k, invariant));
 
-			if (result instanceof SatResult) {
-				Model model = ((SatResult) result).getModel();
+			if (!(result instanceof UnsatResult)) {
+				Model model = getModel(result);
+				if (model == null) {
+					comment("No model - unable to continue");
+					throw new StopException();
+				}
 				invariant.refine(new ModelEvaluator(model, k));
 				comment("Finished single inductive step refinement");
 			}
-		} while (!invariant.isTrivial() && result instanceof SatResult);
+		} while (!invariant.isTrivial() && !(result instanceof UnsatResult));
 
 		solver.pop();