summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2020-03-18 19:00:29 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2020-03-18 19:00:29 -0700
commitc54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4 (patch)
treee226d09670694e76fc73b4ee7dd92b6989a7df21
parent488f949721f3e68edc6028cff40afd8c60f53619 (diff)
downloadabc-c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4.tar.gz
abc-c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4.tar.bz2
abc-c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4.zip
Corner case bug fix in &sat -a.
-rw-r--r--src/proof/cec/cecSolve.c15
1 files changed, 12 insertions, 3 deletions
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index 02f14b76..af6a4fdb 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -673,6 +673,14 @@ p->timeSatUndec += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
+Abc_Cex_t * Cex_ManGenSimple( Cec_ManSat_t * p, int iOut )
+{
+ Abc_Cex_t * pCex;
+ pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
+ pCex->iPo = iOut;
+ pCex->iFrame = 0;
+ return pCex;
+}
Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
{
Abc_Cex_t * pCex;
@@ -715,10 +723,11 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
{
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
{
- pObj->fMark0 = 0;
- pObj->fMark1 = 1;
+ status = !Gia_ObjFaninC0(pObj);
+ pObj->fMark0 = (status == 0);
+ pObj->fMark1 = (status == 1);
if ( pPars->fSaveCexes )
- Vec_PtrWriteEntry( pAig->vSeqModelVec, i, (Abc_Cex_t *)(ABC_PTRINT_T)1 );
+ Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenSimple(p, i) );
continue;
}
Bar_ProgressUpdate( pProgress, i, "SAT..." );