+ TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND))
+ != result[*d_boolTypeNode].end());
+
+ //in bv, we should only have "extract" as an operator.
+ TS_ASSERT(result[*d_boolTypeNode].size() == 2);
+ Node extractOp1 = d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
+ Node extractOp2 = d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
+ TS_ASSERT(result[*d_bvTypeNode].find(extractOp1)
+ != result[*d_bvTypeNode].end());
+ TS_ASSERT(result[*d_bvTypeNode].find(extractOp2)
+ != result[*d_bvTypeNode].end());