From 010d930638cef32aafbb76c8a6e39b335ab0f9e8 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 21 Jul 2014 11:28:40 -0700
Subject: [PATCH] Optimize symbolic "extract" to produce literal value if
 result has width 0

---
 src/Cryptol/Symbolic/BitVector.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Cryptol/Symbolic/BitVector.hs b/src/Cryptol/Symbolic/BitVector.hs
index f924a96d..5b007749 100644
--- a/src/Cryptol/Symbolic/BitVector.hs
+++ b/src/Cryptol/Symbolic/BitVector.hs
@@ -106,6 +106,7 @@ instance SDivisible (SBV BitVector) where
 extract :: Int -> Int -> SWord -> SWord
 extract i j x =
   case x of
+    _ | i < j -> SBV k (Left (CW k (CWInteger 0)))
     SBV _ (Left cw) ->
       case cw of
         CW _ (CWInteger v) -> SBV k (Left (normCW (CW k (CWInteger (v `shiftR` j)))))