more test

SBVTestSuite/GoldFiles/array_misc_13.gold

@@ -0,0 +1,41 @@
+** 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] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () (Array (SBVTuple2 Int 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 s3 () Bool (= s1 s2))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s3)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 ((as const (Array (SBVTuple2 Int Int) (SBVTuple2 Int Int))) (mkSBVTuple2 1 2))))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = ([], (1,2)) :: Array (Integer, Integer) (Integer, Integer)

SBVTestSuite/TestSuite/Arrays/InitVals.hs

@@ -98,6 +98,8 @@ tests = testGroup "Arrays" [
 
       , 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)
+
+      , goldenCapturedIO "array_misc_13" $ t satWith $ \(a :: SArray (Integer, Integer) (Integer, Integer)) -> readArray a (literal (1, 2)) .== literal (1, 2)
       ]
   ]
   where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f