Missing case in BMS.

5b2472d4 · Mathias Soeken · 6d7f2c4d · 5b2472d4
Commit 5b2472d4 authored Sep 09, 2016 by Mathias Soeken
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 1 deletions

src/base/abci/abcExact.c
+4 -1

No files found.
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -1344,7 +1344,10 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
                break;
            case 4: /* OR(!x,g) */
-                assert( 0 ); /* should be impossible since all gates are normal */
+                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
+                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
+                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
+                break;
            case 5: /* XOR(x,g) */
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
                Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );