From b3e6cb30bb9e37e688ac11f6f69156646676c11c Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 27 Apr 2015 13:56:17 -0700
Subject: Bug fix in %read_smt and prevent crash of &cec if there is no current
 AIG.

---
 src/base/abci/abc.c       |  5 +++++
 src/base/wlc/wlcReadSmt.c | 18 ++++++++++++++----
 2 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e9df4ec2..4de17f26 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31034,6 +31034,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no AIG.\n" );
+        return 1;
+    }
     if ( fMiter )
     {
         if ( fDualOutput )
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 4e09306c..0e8e1e06 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -290,10 +290,20 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
     Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
     if ( pStr[0] != '#' ) // decimal
     {
-        int Number = atoi( pStr );
-        nBits = Abc_Base2Log( Number+1 );
-        assert( nBits < 32 );
-        Vec_IntPush( vFanins, Number );
+        if ( pStr[0] >= 0 && pStr[0] <= 9 )
+        {
+            int Number = atoi( pStr );
+            nBits = Abc_Base2Log( Number+1 );
+            assert( nBits < 32 );
+            Vec_IntPush( vFanins, Number );
+        }
+        else
+        {
+            int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
+            assert( fFound );
+            Vec_IntFree( vFanins );
+            return iObj;
+        }
     }
     else if ( pStr[1] == 'b' ) // binary
     {
-- 
cgit v1.2.3