From 101491132fbd617b0a0819045cc7b5d35395706d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 23 Jun 2013 13:28:30 +0200 Subject: [PATCH] Added SAT support for -all/-max with -verify --- passes/sat/sat.cc | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 769d94a07..c75204230 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) { -- 2.30.2