From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 22 Feb 2015 11:42:05 +0000 (+0100)
Subject: Fixed "sat -initsteps" off-by-one bug
X-Git-Tag: yosys-0.6~397
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39d25b212cb0b7ef11aeabea3c19877a31820d98;p=yosys.git

Fixed "sat -initsteps" off-by-one bug
---

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index b998359dd..79d1ec860 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1436,7 +1436,7 @@ struct SatPass : public Pass {
 					if (inductlen > 1)
 						inductstep.force_unique_state(1, inductlen + 1);
 
-					if (inductlen < tempinduct_skip || inductlen < initsteps || inductlen % stepsize != 0)
+					if (inductlen <= tempinduct_skip || inductlen <= initsteps || inductlen % stepsize != 0)
 					{
 						if (inductlen < tempinduct_skip)
 							log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).",