summaryrefslogtreecommitdiffstats
path: root/src/proof/acec/acecNorm.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-01-14 20:28:26 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-01-14 20:28:26 +0700
commit1b86911c4fe0b193c3a281e823de7934664da798 (patch)
tree44e3f3fe59361848443f9952b3247db0b94d80a6 /src/proof/acec/acecNorm.c
parent79701f8b4603596095d3d04a13018c8e9598f7a0 (diff)
downloadabc-1b86911c4fe0b193c3a281e823de7934664da798.tar.gz
abc-1b86911c4fe0b193c3a281e823de7934664da798.tar.bz2
abc-1b86911c4fe0b193c3a281e823de7934664da798.zip
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec/acecNorm.c')
-rw-r--r--src/proof/acec/acecNorm.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 4ed32e7b..0d209524 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -112,7 +112,7 @@ int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
assert( Gia_ObjIsAnd(pObj) );
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
- return (pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
+ return (pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
}
Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits )
{