diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 23:05:36 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 23:05:36 -0800 |
| commit | 75d334a0df1431e8a5a57a83096dcee9661fd0a6 (patch) | |
| tree | ca537311c87658d0524402f0303e26bd245f1251 /src/sat | |
| parent | 7d7ce3ecd03059602f70f26612aabd4a2ec49422 (diff) | |
| download | abc-75d334a0df1431e8a5a57a83096dcee9661fd0a6.tar.gz abc-75d334a0df1431e8a5a57a83096dcee9661fd0a6.tar.bz2 abc-75d334a0df1431e8a5a57a83096dcee9661fd0a6.zip | |
New exact synthesis command 'allexact'.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcMaj3.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c index e35b2e87..8a5b3d16 100644 --- a/src/sat/bmc/bmcMaj3.c +++ b/src/sat/bmc/bmcMaj3.c @@ -948,10 +948,12 @@ static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl ) printf( "(" ); for ( k = 0; k < i; k++ ) if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k)) ) + { if ( k >= 0 && k < p->pPars->nVars ) printf( " %c", 'a'+k ); else printf( " %02d", k ); + } printf( " )\n" ); } } |