From 3b76bc2792e3e0b717d2eca5fc3469d5dfaaab0c Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 12 Jul 2016 13:34:06 -0700
Subject: Bug-fix in SMT-LIB parser (incorrect handling of arithmetic
 right-shift).

---
 src/base/wlc/wlcCom.c     |  4 ++--
 src/base/wlc/wlcReadSmt.c | 22 ++++++++++++++++------
 2 files changed, 18 insertions(+), 8 deletions(-)

(limited to 'src/base')

diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 77bf36ba..5f62f757 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -128,10 +128,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
         switch ( c )
         {
         case 'o':
-            fPrintTree ^= 1;
+            fOldParser ^= 1;
             break;
         case 'p':
-            fOldParser ^= 1;
+            fPrintTree ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index ed6092a5..fcd47274 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -276,13 +276,9 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in
     assert( fSigned >= 0 );
     Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
     if ( fSigned )
-    {
         Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
-//        if ( Vec_IntSize(vFanins) > 0 )
-//            Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned;
-//        if ( Vec_IntSize(vFanins) > 1 )
-//            Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
-    }
+    if ( Type == WLC_OBJ_SHIFT_RA )
+        Wlc_NtkObj(pNtk, iObj)->Signed = 1;
     if ( pName == NULL )
     {
         sprintf( Buffer, "_n%d_", iObj );
@@ -511,6 +507,13 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
         // skip ()
         Fan = Vec_IntEntry(vFans, 2);
         assert( !Smt_EntryIsName(Fan) );
+        vFans2 = Smt_VecEntryNode(p, vFans, 2);
+        if ( Vec_IntSize(vFans2) > 0 )
+        {
+            printf( "File parsing error: Uninterpreted functions are not supported.\n" );
+            Wlc_NtkFree( pNtk ); pNtk = NULL;
+            goto finish;
+        }
         // check type (Bool or BitVec)
         Fan = Vec_IntEntry(vFans, 3);
         if ( Smt_EntryIsName(Fan) ) 
@@ -921,6 +924,13 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
             // skip ()
             Fan = Vec_IntEntry(vFans, 2);
             assert( !Smt_EntryIsName(Fan) );
+            vFans2 = Smt_VecEntryNode(p, vFans, 2);
+            if ( Vec_IntSize(vFans2) > 0 )
+            {
+                printf( "File parsing error: Uninterpreted functions are not supported.\n" );
+                Wlc_NtkFree( pNtk ); pNtk = NULL;
+                goto finish;
+            }
             // check type (Bool or BitVec)
             Fan = Vec_IntEntry(vFans, 3);
             if ( Smt_EntryIsName(Fan) ) 
-- 
cgit v1.2.3