handle BitVectorSignExtend in pickler

diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index 3d077502d320e2a22192ca418449750cd3062236..14477f3cdbb9000336b5f8c16157fa6ad5827aec 100644 (file)
--- 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);
   }