From 6d088bc440fb6b7a5b3eb2c9ea7b9950a1698166 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 3 Feb 2017 17:02:36 -0800
Subject: Enabling new X-valued simulation in 'pdr'.

---
 src/proof/pdr/pdrSat.c | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/proof/pdr/pdrSat.c')

diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index eb94a826..49b0448a 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -377,7 +377,14 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
         p->tSatSat += clk;
         p->nCallsS++;
         if ( ppPred )
-            *ppPred = Pdr_ManTernarySim( p, k, pCube );
+        {
+            abctime clk = Abc_Clock();
+            if ( p->pPars->fNewXSim )
+                *ppPred = Txs_ManTernarySim( p->pTxs, k, pCube );
+            else
+                *ppPred = Pdr_ManTernarySim( p, k, pCube );
+            p->tTsim += Abc_Clock() - clk;
+        }
         RetValue = 0;
     }
 
-- 
cgit v1.2.3