Add a test case for issue #1210

This bug was fixed in What4 via GaloisInc/what4#127
which was included in What4 version 1.2.

Fixes #1210

tests/issues/issue1210.cry

@@ -0,0 +1,15 @@
+mwe : [2] -> [2][1] -> Bit
+property mwe i r = r@0 == (r@0) << 0*i
+
+mwe' : [2] -> [1] -> Bit
+property mwe' i r = r == (r << 0*i)
+
+mwe'' : Bit
+property mwe'' = r == (r << i)
+ where r = 1:[1]
+       i = 0:[2]
+
+bitget : [12] -> [436][8] -> Bit
+property bitget i r = i < 3488 ==> bit_gf == if bit_bit then 0x0001 else 0x0000
+  where bit_gf = (zext (((r@(i/8)) >> (i%8) ) && 1))
+        bit_bit = (join (map reverse r))@i

tests/issues/issue1210.icry

@@ -0,0 +1,6 @@
+:l issue1210.cry
+:check
+:set prover=sbv-z3
+:prove
+:set prover=w4-z3
+:prove

tests/issues/issue1210.icry.stdout

@@ -0,0 +1,31 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property mwe Using exhaustive testing.
+Testing... Passed 16 tests.
+Q.E.D.
+property mwe' Using exhaustive testing.
+Testing... Passed 8 tests.
+Q.E.D.
+property mwe'' Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property bitget Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^3500 values)
+:prove mwe
+	Q.E.D.
+:prove mwe'
+	Q.E.D.
+:prove mwe''
+	Q.E.D.
+:prove bitget
+	Q.E.D.
+:prove mwe
+	Q.E.D.
+:prove mwe'
+	Q.E.D.
+:prove mwe''
+	Q.E.D.
+:prove bitget
+	Q.E.D.