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

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index d89c75506ee6571201bd6efcfe59f9c8ff22107d..9404a0d77b1693845ddf6d1a3e062322f434e809 100644 (file)
--- 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);