From fc5281b3f7656dd5e245f4ab7d81f39a14693f6b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Sep 2016 17:35:25 +0200 Subject: [PATCH] Run log_flush() before solving in sat command --- passes/sat/sat.cc | 3 +++ 1 file changed, 3 insertions(+) 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()) { -- 2.30.2