From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 6 Sep 2016 15:35:25 +0000 (+0200)
Subject: Run log_flush() before solving in sat command
X-Git-Tag: yosys-0.7~77
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc5281b3f7656dd5e245f4ab7d81f39a14693f6b;p=yosys.git

Run log_flush() before solving in sat command
---

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 79e590a36..a6ac7afd4 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1447,6 +1447,7 @@ struct SatPass : public Pass {
 					{
 						log("\n[base case %d] Solving problem with %d variables and %d clauses..\n",
 								inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+						log_flush();
 
 						if (basecase.solve(basecase.ez->NOT(property))) {
 							log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
@@ -1517,6 +1518,7 @@ struct SatPass : public Pass {
 
 						log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
 								inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+						log_flush();
 
 						if (!inductstep.solve(inductstep.ez->NOT(property))) {
 							if (inductstep.gotTimeout)
@@ -1622,6 +1624,7 @@ struct SatPass : public Pass {
 		rerun_solver:
 			log("\nSolving problem with %d variables and %d clauses..\n",
 					sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
+			log_flush();
 
 			if (sathelper.solve())
 			{