From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 23 Jun 2013 11:28:30 +0000 (+0200)
Subject: Added SAT support for -all/-max with -verify
X-Git-Tag: yosys-0.2.0~561
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=101491132fbd617b0a0819045cc7b5d35395706d;p=yosys.git

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

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) {