summaryrefslogtreecommitdiffstats
path: root/src/proof/cec/cecCore.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-08-12 18:54:43 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-08-12 18:54:43 -0700
commitf907347484874a4c5ff9ffdde9426e0229fac22d (patch)
tree8c26bb12e6c080ccdeee17cf38b4324558cc639a /src/proof/cec/cecCore.c
parent9055265394006a1c14688a018db48d06ba14e756 (diff)
downloadabc-f907347484874a4c5ff9ffdde9426e0229fac22d.tar.gz
abc-f907347484874a4c5ff9ffdde9426e0229fac22d.tar.bz2
abc-f907347484874a4c5ff9ffdde9426e0229fac22d.zip
Enabling circuit solver in &fraig.
Diffstat (limited to 'src/proof/cec/cecCore.c')
-rw-r--r--src/proof/cec/cecCore.c5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index c77b8fa1..71335e85 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -426,7 +426,10 @@ p->timeSim += Abc_Clock() - clk;
break;
}
clk = Abc_Clock();
- Cec_ManSatSolve( pPat, pSrm, pParsSat );
+ if ( pPars->fRunCSat )
+ Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
+ else
+ Cec_ManSatSolve( pPat, pSrm, pParsSat );
p->timeSat += Abc_Clock() - clk;
if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
{