From 9c5a63c52c24f0570557b4bf7340b41666cf44b6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 24 Aug 2014 13:27:40 +0200 Subject: [PATCH] azonenberg: Make dump_vcd save model when temporal induction fails due to step limit --- passes/sat/sat.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index c6da4bb42..08ae9e929 100644 --- 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: