From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 21 Feb 2015 19:05:16 +0000 (+0100)
Subject: When "sat -tempinduct-baseonly -maxsteps N" reaches maxsteps it is a good thing.
X-Git-Tag: yosys-0.6~400
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9237fb924e74a0ed687992df6988b4aa2105614e;p=yosys.git

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 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);