summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-02-22 12:42:05 +0100
committerClifford Wolf <clifford@clifford.at>2015-02-22 12:42:05 +0100
commit39d25b212cb0b7ef11aeabea3c19877a31820d98 (patch)
treed972a9677b25560e4fd00ffb8af1a789231a9d55 /passes
parentfae0e75ace66d77eaf434305bdb06ca29931ec7b (diff)
Fixed "sat -initsteps" off-by-one bug
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc2
1 files changed, 1 insertions, 1 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index b998359d..79d1ec86 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).",