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 ...
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;
for (uint l = 0; l < problems.getSize(); l++) {
Problem *problem = problems.get(l);
long long time1 = tuner1->getTime(problem);
- if(time1 == -1){
+ if(time1 == -1 || time2 == -2){
time1=LLONG_MAX;
}
long long time2 = tuner2->getTime(problem);
- if(time2 == -1){
+ if(time2 == -1 || time2 == -2){
time2 = LLONG_MAX;
}
mintimes[l] = pow(min(time1,time2), (double)1 / problems.getSize());