diff --git a/src/main/java/de/stups/probkodkod/ImmutableProblem.java b/src/main/java/de/stups/probkodkod/ImmutableProblem.java
index fc27cd80195a5606b4659168fa7b2415b51d84d6..6668dc08b22423c797c5e7e640cecf0a09f85085 100644
--- a/src/main/java/de/stups/probkodkod/ImmutableProblem.java
+++ b/src/main/java/de/stups/probkodkod/ImmutableProblem.java
@@ -198,7 +198,7 @@ public final class ImmutableProblem {
 				logger.info(bounds.toString());
 			}
 
-			return new Request(variables, Arrays.asList(sol).iterator());
+			return new Request(variables, new NonIncrementalSolverSolutionIterator(sol));
 		}
 	}
 
diff --git a/src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java b/src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java
new file mode 100644
index 0000000000000000000000000000000000000000..d5b606cb8ee58937f244f311b5c4752ad14a983c
--- /dev/null
+++ b/src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java
@@ -0,0 +1,29 @@
+package de.stups.probkodkod;
+
+import java.util.Iterator;
+
+import kodkod.engine.Solution;
+
+public class NonIncrementalSolverSolutionIterator implements Iterator<Solution> {
+
+	private Solution sol;
+	private boolean returned = false;
+
+	public NonIncrementalSolverSolutionIterator(Solution sol) {
+		this.sol = sol;
+	}
+
+	@Override
+	public boolean hasNext() {
+		return true;
+	}
+
+	@Override
+	public Solution next() {
+		if (!returned) {
+			return sol;
+		}
+		throw new RuntimeException("second solution of non-incremental solver requested");
+	}
+
+}
diff --git a/src/main/java/de/stups/probkodkod/Request.java b/src/main/java/de/stups/probkodkod/Request.java
index beb001277045d68ac7bdeaf7551746a67df558f5..6a2d17feaa91e132904309d24f3392c3f839b37d 100644
--- a/src/main/java/de/stups/probkodkod/Request.java
+++ b/src/main/java/de/stups/probkodkod/Request.java
@@ -7,14 +7,13 @@ import java.util.Map;
 import java.util.logging.Level;
 import java.util.logging.Logger;
 
+import de.prob.prolog.output.IPrologTermOutput;
+import de.stups.probkodkod.types.TupleType;
 import kodkod.ast.Relation;
 import kodkod.engine.Solution;
-import kodkod.engine.Statistics;
 import kodkod.instance.Instance;
 import kodkod.instance.Tuple;
 import kodkod.instance.TupleSet;
-import de.prob.prolog.output.IPrologTermOutput;
-import de.stups.probkodkod.types.TupleType;
 
 /**
  * A request stores the information about a ongoing query in the current
@@ -29,13 +28,11 @@ public final class Request {
 	private final RelationInfo[] variables;
 	private final Iterator<Solution> iterator;
 
-	public Request(final RelationInfo[] variables,
-			final Iterator<Solution> iterator) {
+	public Request(final RelationInfo[] variables, final Iterator<Solution> iterator) {
 		this.variables = variables;
 		this.iterator = iterator;
 		if (logger.isLoggable(Level.FINE)) {
-			logger.fine("request created: return variables are: "
-					+ Arrays.asList(variables));
+			logger.fine("request created: return variables are: " + Arrays.asList(variables));
 		}
 	}
 
@@ -95,8 +92,7 @@ public final class Request {
 			pto.closeTerm();
 			pto.fullstop();
 			if (logger.isLoggable(Level.FINE)) {
-				logger.fine("wrote " + num + " solutions, computed in "
-						+ duration + "ms");
+				logger.fine("wrote " + num + " solutions, computed in " + duration + "ms");
 			}
 			return solutionsPresent;
 		} catch (RuntimeException ex) {
@@ -106,6 +102,11 @@ public final class Request {
 				pto.fullstop();
 				return true;
 			}
+			if ("second solution of non-incremental solver requested".equals(ex.getMessage())) {
+				pto.printAtom("sat_non_incremental");
+				pto.fullstop();
+				return true;
+			}
 			throw (ex);
 		}
 	}
@@ -117,14 +118,12 @@ public final class Request {
 				pto.openList();
 				for (int i = 0; i < variables.length; i++) {
 					final RelationInfo relinfo = variables[i];
-					final TupleSet tupleSet = instance.tuples(relinfo
-							.getRelation());
+					final TupleSet tupleSet = instance.tuples(relinfo.getRelation());
 					final TupleType tupleType = relinfo.getTupleType();
 					pto.openTerm(tupleType.isSingleton() ? "b" : "s");
 					pto.printAtom(relinfo.getId());
 					if (tupleType.isSingleton()) {
-						final Tuple tuple = tupleSet.isEmpty() ? null
-								: tupleSet.iterator().next();
+						final Tuple tuple = tupleSet.isEmpty() ? null : tupleSet.iterator().next();
 						writeTuple(pto, tupleType, tupleSet, tuple);
 					} else {
 						pto.openList();
@@ -139,15 +138,13 @@ public final class Request {
 		pto.closeList();
 	}
 
-	private void writeTupleSet(final IPrologTermOutput pto,
-			final TupleType tupleType, final TupleSet tupleSet) {
+	private void writeTupleSet(final IPrologTermOutput pto, final TupleType tupleType, final TupleSet tupleSet) {
 		for (Tuple tuple : tupleSet) {
 			writeTuple(pto, tupleType, tupleSet, tuple);
 		}
 	}
 
-	private void writeTuple(final IPrologTermOutput pto,
-			final TupleType tupleType, final TupleSet tupleSet,
+	private void writeTuple(final IPrologTermOutput pto, final TupleType tupleType, final TupleSet tupleSet,
 			final Tuple tuple) {
 		final int[] intTuple = tupleType.decodeTuple(tuple, tupleSet);
 		pto.openList();
@@ -163,20 +160,19 @@ public final class Request {
 			Solution solution = iterator.next();
 			instance = solution.instance();
 			if (logger.isLoggable(Level.FINE)) {
-				logger.fine("CNF translated in " + solution.stats().translationTime()
-				        + " ms and solved in " + solution.stats().solvingTime() + "ms ("
-			            + solution.stats().clauses() + " clauses, "
-						+ solution.stats().variables() + " variables, "
-						+ solution.stats().primaryVariables() + " primary variables)");
+				logger.fine("CNF translated in " + solution.stats().translationTime() + " ms and solved in "
+						+ solution.stats().solvingTime() + "ms (" + solution.stats().clauses() + " clauses, "
+						+ solution.stats().variables() + " variables, " + solution.stats().primaryVariables()
+						+ " primary variables)");
 			}
-					/* TO DO: maybe add a preference for this: */
-					/* the information is printed on the output stream and then
-					   read by ProB in get_solutions_from_stream in kodkod_process.pl */
-			System.out.println("stats(" + solution.stats().translationTime() +
-					  "," + solution.stats().solvingTime() +
-					  "," + solution.stats().clauses() +
-					  "," + solution.stats().variables() +
-					  "," + solution.stats().primaryVariables() + "). ");
+			/* TO DO: maybe add a preference for this: */
+			/*
+			 * the information is printed on the output stream and then read by
+			 * ProB in get_solutions_from_stream in kodkod_process.pl
+			 */
+			System.out.println("stats(" + solution.stats().translationTime() + "," + solution.stats().solvingTime()
+					+ "," + solution.stats().clauses() + "," + solution.stats().variables() + ","
+					+ solution.stats().primaryVariables() + "). ");
 		} else {
 			instance = null;
 		}