more tests

SBVTestSuite/GoldFiles/array_misc_28.gold

@@ -0,0 +1,34 @@
+** 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-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s1 () Int 3)
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Int)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s2 () Bool (= s0 s1))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s2)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 3))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = 3 :: Integer

SBVTestSuite/GoldFiles/array_misc_29.gold

@@ -0,0 +1,34 @@
+** 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-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s1 () Int 3)
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Int)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s2 () Bool (= s0 s1))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s2)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 3))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = 3 :: Integer

SBVTestSuite/GoldFiles/array_misc_30.gold

@@ -0,0 +1,34 @@
+** 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-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s1 () Int 3)
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Int)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s2 () Bool (= s0 s1))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s2)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 3))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = 3 :: Integer

SBVTestSuite/TestSuite/Arrays/InitVals.hs

@@ -118,6 +118,10 @@ tests = testGroup "Arrays" [
       , goldenCapturedIO "array_misc_25" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float                Integer) (1/0))
       , goldenCapturedIO "array_misc_26" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double               Integer) (1/0))
       , goldenCapturedIO "array_misc_27" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (1/0))
+
+      , goldenCapturedIO "array_misc_28" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float                Integer) (-1/0))
+      , goldenCapturedIO "array_misc_29" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double               Integer) (-1/0))
+      , goldenCapturedIO "array_misc_30" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-1/0))
       ]
   ]
   where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f