Bug fix: typos
[satune.git] / src / Tuner / basictuner.cc
index 44cd2bc8b3eee8b0b7479e8a2062397946c4caf7..6ac7453a249648a16fcb93c3850d1ef8d2250e68 100644 (file)
@@ -157,7 +157,7 @@ long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
        uint timeinsecs = problem->getBestTime() / NANOSEC;
        uint adaptive = (timeinsecs > 30) ? timeinsecs * 5 : 150;
        uint maxtime = (adaptive < timeout) ? adaptive : timeout;
-       uint satuneTimeout = 2 * maxtime;
+       uint satuneTimeout = (2*maxtime < maxtime + 600)?2*maxtime: maxtime + 600;
        //Do run
        snprintf(buffer, sizeof(buffer), "timeout %u ./run.sh deserializerun %s %u tuner%u result%u > log%u", satuneTimeout, problem->getProblem(), maxtime, execnum, execnum, execnum);
        model_print("Running: %s\n", buffer);
@@ -179,7 +179,9 @@ long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
                        myfile >> sat;
                        myfile.close();
                }
-               updateTimeout(problem, metric);
+               if(sat != IS_INDETER){
+                       updateTimeout(problem, metric);
+               }
                snprintf(buffer, sizeof(buffer), "tuner%uused", execnum);
                tuner->getTuner()->addUsed(buffer);
        } else if (status == 124 << 8) {// timeout happens ...
@@ -192,7 +194,8 @@ long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
        if (problem->getResult() == TUNERUNSETVALUE && sat != IS_INDETER) {
                problem->setResult( sat );
        } else if (problem->getResult() != sat && sat != IS_INDETER) {
-               model_print("******** Result has changed ********\n");
+               model_print("******** Result has changed ******** Found a bug!!\n");
+               ASSERT(0);
        }
        if (sat == IS_INDETER && metric != -1) {//The case when we have a timeout
                metric = -1;