Version abc50904

1 files changed, 15 insertions, 3 deletions

diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index da9e8e2b..17201e58 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -122,11 +122,23 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 ***********************************************************************/
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
-    if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
+    Fraig_Node_t * pNode;
+    FREE( p->pModel );
+    // get the output node (it can be complemented!)
+    pNode = p->vOutputs->pArray[0];
+    // if the miter is constant 0, the problem is UNSAT
+    if ( pNode == Fraig_Not(p->pConst1) )
         return 1;
+    // consider the special case when the miter is constant 1
+    if ( pNode == p->pConst1 )
+    {
+        // in this case, any counter example will do to distinquish it from constant 0
+        // here we pick the counter example composed of all zeros
+        p->pModel = Fraig_ManAllocCounterExample( p );
+        return 0;
+    }
     // save the counter example
-    FREE( p->pModel );
-    p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
+    p->pModel = Fraig_ManSaveCounterExample( p, pNode );
     // if the model is not found, return undecided
     if ( p->pModel == NULL )
         return -1;