When "sat -tempinduct-baseonly -maxsteps N" reaches maxsteps it is a good thing.

This commit is contained in:
Clifford Wolf 2015-02-21 20:05:16 +01:00
parent 1688b9b464
commit 9237fb924e
1 changed files with 5 additions and 0 deletions

View File

@ -1438,6 +1438,11 @@ struct SatPass : public Pass {
}
}
if (tempinduct_baseonly) {
log("\nReached maximum number of time steps -> proved base case for %d steps: SUCCESS!\n", maxsteps);
goto tip_success;
}
log("\nReached maximum number of time steps -> proof failed.\n");
if(!vcd_file_name.empty())
inductstep.dump_model_to_vcd(vcd_file_name);