Added SAT support for -all/-max with -verify

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 769d94a073e333e8e4843be14806b7c071ec927f..c75204230ceb83ddf692f3ffa379d26727908d3b 100644 (file)
--- 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) {