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

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index b998359dde010213eced2c2f78c99c8718ef46cd..79d1ec8600c892007a2917e9d75ed15cc827e96c 100644 (file)
--- 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).",