From 9237fb924e74a0ed687992df6988b4aa2105614e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 21 Feb 2015 20:05:16 +0100
Subject: [PATCH] When "sat -tempinduct-baseonly -maxsteps N" reaches maxsteps
 it is a good thing.

---
 passes/sat/sat.cc | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index d89c75506..9404a0d77 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);