X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Finc_solver.cc;h=de88f1937b8a2da76a3c4308f0ebe470a3d8e19e;hb=HEAD;hp=2d6b8a48d993aa6ad9164e2060b413c50533e0b6;hpb=1038eba14663554fb228406db8f33a8ead28b89b;p=satune.git

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 2d6b8a4..de88f19 100644
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -102,6 +102,18 @@ int getSolution(IncrementalSolver *This) {
 		}
 		readSolver(This, &This->solution[1], numVars * sizeof(int));
 		This->solutionsize = numVars;
+	} else if (result == IS_INDETER){
+		return result;	
+	} else {//Reading unsat explanation
+		int numVars = readIntSolver(This);
+		if (numVars > This->solutionsize) {
+			if (This->solution != NULL)
+				ourfree(This->solution);
+			This->solution = (int *) ourmalloc((numVars + 1) * sizeof(int));
+			This->solution[0] = 0;
+		}
+		readSolver(This, &This->solution[1], numVars * sizeof(int));
+		This->solutionsize = numVars;
 	}
 	return result;
 }