From afc984d28606e0c3c0254a26033f4a934eebd5b7 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 8 Jun 2012 10:18:01 +0000
Subject: [PATCH] handle BitVectorSignExtend in pickler

---
 src/expr/pickler.cpp | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index 3d077502d..14477f3cd 100644
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -233,6 +233,12 @@ void PicklerPrivate::toCaseConstant(TNode n) {
     toCaseString(k, asString);
     break;
   }
+  case  kind::BITVECTOR_SIGN_EXTEND_OP: {
+    BitVectorSignExtend bvse = n.getConst<BitVectorSignExtend>();
+    d_current << mkConstantHeader(k, 1);
+    d_current << mkBlockBody(bvse.signExtendAmount);
+    break;
+  }
   default:
     Unhandled(k);
   }
@@ -371,6 +377,11 @@ Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) {
     BitVector bv(size, value);
     return d_nm->mkConst(bv);
   }
+  case  kind::BITVECTOR_SIGN_EXTEND_OP: {
+    Block signExtendAmount = d_current.dequeue();
+    BitVectorSignExtend bvse(signExtendAmount.d_body.d_data);
+    return d_nm->mkConst<BitVectorSignExtend>(bvse);
+  }
   default:
     Unhandled(k);
   }
-- 
2.30.2