Bug fixes for Java API + Exactly one constraints + Adding support for getting the...

[satune.git] / src / Backend / inc_solver.cc

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 2d6b8a48d993aa6ad9164e2060b413c50533e0b6..72d34083dcd4b096b32aee4b51816a361f708600 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -102,6 +102,16 @@ int getSolution(IncrementalSolver *This) {
                }
                readSolver(This, &This->solution[1], numVars * sizeof(int));
                This->solutionsize = numVars;
+       } 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;
 }