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

1 files changed, 5 insertions, 0 deletions

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index d89c7550..9404a0d7 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -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);