X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FTuner%2Fbasictuner.cc;h=f3a00ea460aa1d78dd627805782993b73aa9bffd;hp=30d729b2cb2c12d0a7842e78b4db45505fc0a6a5;hb=cb7331d3834636ca4af0357d272d082c047ec940;hpb=48d6d13304d821220f063f05683d977160826177 diff --git a/src/Tuner/basictuner.cc b/src/Tuner/basictuner.cc index 30d729b..f3a00ea 100644 --- a/src/Tuner/basictuner.cc +++ b/src/Tuner/basictuner.cc @@ -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;