diff --git a/SBVTestSuite/GoldFiles/array_misc_11.gold b/SBVTestSuite/GoldFiles/array_misc_11.gold
new file mode 100644
index 000000000..67ff72479
--- /dev/null
+++ b/SBVTestSuite/GoldFiles/array_misc_11.gold
@@ -0,0 +1,42 @@
+** Calling: z3 -nw -in -smt2
+[GOOD] ; Automatically generated by SBV. Do not edit.
+[GOOD] (set-option :print-success true)
+[GOOD] (set-option :global-declarations true)
+[GOOD] (set-option :smtlib2_compliant true)
+[GOOD] (set-option :diagnostic-output-channel "stdout")
+[GOOD] (set-option :produce-models true)
+[GOOD] (set-option :pp.max_depth      4294967295)
+[GOOD] (set-option :pp.min_alias_size 4294967295)
+[GOOD] (set-option :model.inline_def  true      )
+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
+                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
+                                                         (proj_2_SBVTuple2 T2))))))
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s1 () (SBVTuple2 Int Int) (mkSBVTuple2 1 2))
+[GOOD] (define-fun s3 () Int 3)
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () (Array (SBVTuple2 Int Int) Int))
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s2 () Int (select s0 s1))
+[GOOD] (define-fun s4 () Bool (= s2 s3))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s4)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 ((as const (Array (SBVTuple2 Int Int) Int)) 3)))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = ([], 3) :: Array (Integer, Integer) Integer
diff --git a/SBVTestSuite/GoldFiles/array_misc_12.gold b/SBVTestSuite/GoldFiles/array_misc_12.gold
new file mode 100644
index 000000000..0ca5be235
--- /dev/null
+++ b/SBVTestSuite/GoldFiles/array_misc_12.gold
@@ -0,0 +1,42 @@
+** Calling: z3 -nw -in -smt2
+[GOOD] ; Automatically generated by SBV. Do not edit.
+[GOOD] (set-option :print-success true)
+[GOOD] (set-option :global-declarations true)
+[GOOD] (set-option :smtlib2_compliant true)
+[GOOD] (set-option :diagnostic-output-channel "stdout")
+[GOOD] (set-option :produce-models true)
+[GOOD] (set-option :pp.max_depth      4294967295)
+[GOOD] (set-option :pp.min_alias_size 4294967295)
+[GOOD] (set-option :model.inline_def  true      )
+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
+                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
+                                                         (proj_2_SBVTuple2 T2))))))
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s1 () Int 3)
+[GOOD] (define-fun s3 () (SBVTuple2 Int Int) (mkSBVTuple2 1 2))
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () (Array Int (SBVTuple2 Int Int)))
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s2 () (SBVTuple2 Int Int) (select s0 s1))
+[GOOD] (define-fun s4 () Bool (= s2 s3))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s4)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 ((as const (Array Int (SBVTuple2 Int Int))) (mkSBVTuple2 1 2))))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = ([], (1,2)) :: Array Integer (Integer, Integer)
diff --git a/SBVTestSuite/TestSuite/Arrays/InitVals.hs b/SBVTestSuite/TestSuite/Arrays/InitVals.hs
index ae2ad233b..0e3e9aa7d 100644
--- a/SBVTestSuite/TestSuite/Arrays/InitVals.hs
+++ b/SBVTestSuite/TestSuite/Arrays/InitVals.hs
@@ -95,6 +95,9 @@ tests = testGroup "Arrays" [
 
       , testCase         "array_misc_10" $                   (write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
                                                           .== write (empty 0) [(i, i  ) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "False"
+
+      , goldenCapturedIO "array_misc_11" $ t satWith $ \(a :: SArray (Integer, Integer) Integer) -> readArray a (literal (1, 2)) .== 3
+      , goldenCapturedIO "array_misc_12" $ t satWith $ \(a :: SArray Integer (Integer, Integer)) -> readArray a 3 .== literal (1, 2)
       ]
   ]
   where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f