diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2022-04-24 10:25:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2022-04-24 10:25:46 -0700 |
| commit | 1abd0457abb9f522da48e24996545b155285bac9 (patch) | |
| tree | 5e4ab018f7dcefbbce6a93bb81b6aa054456a639 /src/proof | |
| parent | cb30ea0516cf85b839794c4755f6071a02e55537 (diff) | |
| download | abc-1abd0457abb9f522da48e24996545b155285bac9.tar.gz abc-1abd0457abb9f522da48e24996545b155285bac9.tar.bz2 abc-1abd0457abb9f522da48e24996545b155285bac9.zip | |
Experiments with SAT sweeping.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecSatG3.c | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/proof/cec/cecSatG3.c b/src/proof/cec/cecSatG3.c index bdfa0f90..eaad455b 100644 --- a/src/proof/cec/cecSatG3.c +++ b/src/proof/cec/cecSatG3.c @@ -1564,9 +1564,8 @@ void Cec5_ManLoadInstance( Cec5_Man_t * p, int iObj0, int iObj1, int * piVar0, i int iVar1 = Cec5_ObjGetCnfVar( p, iObj1 ); if( p->pPars->jType > 0 ) { - extern void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ); int nlim = p->approxLim; - glucose2_markapprox( p->pSat, iVar0, iVar1, nlim ); + bmcg2_sat_solver_markapprox( p->pSat, iVar0, iVar1, nlim ); } * piVar0 = iVar0; |