From 10ad89490a6596dc51e27b6d7ebd0f2f0c606ed8 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 6 Jan 2012 11:34:06 +0700
Subject: Bug fix related to not properly resizing SAT solver's model array.

---
 src/aig/int/intContain.c | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/aig/int/intContain.c')

diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index d4af0ae8..77b057a7 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -274,7 +274,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
     int Counter;
     if ( nFrames == 1 )
         return 1;
-    if ( pSat->model.size == 0 )
+//    if ( pSat->model.size == 0 )
+    
+    // possible consequences here!!!
+    assert( 0 );
+
+    if ( sat_solver_nvars(pSat) == 0 )
         return 1;
 //    assert( Saig_ManPoNum(p) == 1 );
     assert( Aig_ManRegNum(p) > 0 );
-- 
cgit v1.2.3