diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-08-24 13:27:40 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-08-24 13:27:40 +0200 |
| commit | 9c5a63c52c24f0570557b4bf7340b41666cf44b6 (patch) | |
| tree | 7221be2d621e239f36dfcbaab0ef177793c81939 | |
| parent | c642dd0b3eb1390b6c1acd39c1f19797da27b190 (diff) | |
azonenberg: Make dump_vcd save model when temporal induction fails due to step limit
| -rw-r--r-- | passes/sat/sat.cc | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index c6da4bb4..08ae9e92 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: |