Commit 74e445ad by Mathias Soeken

Exact synthesis.

parent 574cf102
...@@ -1428,7 +1428,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) ...@@ -1428,7 +1428,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{ {
pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, k ), 1 ); pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, k ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, iii, i, ii ), 1 ); pLits[2] = Abc_Var2Lit( Ses_ManSelectVar( pSes, iii, i, ii ), 1 );
sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment