Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 1eba56d4bd46afdfa886a9e7b5efbfaa361360a2..cd2ec550aae443580cc9fac82b0d9f918aa0b174 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -605,6 +605,9 @@ void CSolver::inferFixedOrders() {
 }
 
 int CSolver::solve() {
+       if(isUnSAT()){
+               return IS_UNSAT;
+       }
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
@@ -660,7 +663,7 @@ int CSolver::solve() {
 
                time2 = getTimeNano();
                model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
+               
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();