diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-09-06 17:35:25 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-09-06 17:35:25 +0200 |
| commit | fc5281b3f7656dd5e245f4ab7d81f39a14693f6b (patch) | |
| tree | e52e4c3fc5e678c6e7c26b918f7e36c8634daa28 /passes/sat/sat.cc | |
| parent | d55a93b39ff331aea16d627de92b1cbee2be68db (diff) | |
| download | yosys-fc5281b3f7656dd5e245f4ab7d81f39a14693f6b.tar.gz yosys-fc5281b3f7656dd5e245f4ab7d81f39a14693f6b.tar.bz2 yosys-fc5281b3f7656dd5e245f4ab7d81f39a14693f6b.zip | |
Run log_flush() before solving in sat command
Diffstat (limited to 'passes/sat/sat.cc')
| -rw-r--r-- | passes/sat/sat.cc | 3 |
1 files changed, 3 insertions, 0 deletions
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()) { |