diff options
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/sat/sat.cc | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 769d94a0..c7520423 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -659,7 +659,7 @@ struct SatPass : public Pass { } else { - if (loopcount > 0) + if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); SatHelper sathelper(design, module); @@ -702,16 +702,16 @@ struct SatPass : public Pass { sathelper.print_model(); - if (verify) { - log("\n"); - log_error("Called with -verify and proof did fail!\n"); - } - if (loopcount != 0) { loopcount--, did_rerun = true; sathelper.invalidate_model(); goto rerun_solver; } + + if (verify) { + log("\n"); + log_error("Called with -verify and proof did fail!\n"); + } } else { @@ -726,6 +726,11 @@ struct SatPass : public Pass { print_qed(); } } + + if (verify && did_rerun) { + log("\n"); + log_error("Called with -verify and proof did fail!\n"); + } } if (0) { |