riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Run log_flush() before solving in sat command

This commit is contained in:
Clifford Wolf 2016-09-06 17:35:25 +02:00
parent d55a93b39f
commit fc5281b3f7
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
passes/sat/sat.cc
View File

@ -1447,6 +1447,7 @@ struct SatPass : public Pass {
{ {
log("\n[base case %d] Solving problem with %d variables and %d clauses..\n", log("\n[base case %d] Solving problem with %d variables and %d clauses..\n",
inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses()); inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
log_flush();
if (basecase.solve(basecase.ez->NOT(property))) { if (basecase.solve(basecase.ez->NOT(property))) {
log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); 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", log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
log_flush();
if (!inductstep.solve(inductstep.ez->NOT(property))) { if (!inductstep.solve(inductstep.ez->NOT(property))) {
if (inductstep.gotTimeout) if (inductstep.gotTimeout)
@ -1622,6 +1624,7 @@ struct SatPass : public Pass {
rerun_solver: rerun_solver:
log("\nSolving problem with %d variables and %d clauses..\n", log("\nSolving problem with %d variables and %d clauses..\n",
sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses()); sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
log_flush();
if (sathelper.solve()) if (sathelper.solve())
{ {