From c39fd3741a777034a2cbef247a1097222ac789b6 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 23 Jan 2012 12:41:55 -0800
Subject: Added returning counter-example after BMC, which was recently added
 to 'dprove'.

---
 src/base/abci/abcDar.c | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/base/abci/abcDar.c')

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index b032b4e4..6b8cd378 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2270,6 +2270,10 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
                 printf( "SOLUTION: FAIL       " );
                 ABC_PRT( "Time", clock() - clkTotal );
             }
+            // return the counter-example generated
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
+            pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
             Aig_ManStop( pMan );
             return RetValue;
         }
-- 
cgit v1.2.3