azonenberg: Make dump_vcd save model when temporal induction fails due to step limit

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index c6da4bb42bc9d3685cef2d11bbfa65a13f1a1928..08ae9e92978427d7a348fa625ce7ca83be993abc 100644 (file)
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1320,6 +1320,8 @@ struct SatPass : public Pass {
                        }
 
                        log("\nReached maximum number of time steps -> proof failed.\n");
+                       if(!vcd_file_name.empty())
+                               inductstep.dump_model_to_vcd(vcd_file_name);
                        print_proof_failed();
 
                tip_failed: