From 60923da4be755b55ccec4486175d9891756e211f Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Wed, 18 Sep 2024 09:23:47 -0700 Subject: [PATCH] more test --- SBVTestSuite/GoldFiles/array_misc_13.gold | 41 +++++++++++++++++++++++ SBVTestSuite/TestSuite/Arrays/InitVals.hs | 2 ++ 2 files changed, 43 insertions(+) create mode 100644 SBVTestSuite/GoldFiles/array_misc_13.gold diff --git a/SBVTestSuite/GoldFiles/array_misc_13.gold b/SBVTestSuite/GoldFiles/array_misc_13.gold new file mode 100644 index 000000000..efc56582e --- /dev/null +++ b/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) diff --git a/SBVTestSuite/TestSuite/Arrays/InitVals.hs b/SBVTestSuite/TestSuite/Arrays/InitVals.hs index 0e3e9aa7d..eeb43f709 100644 --- a/SBVTestSuite/TestSuite/Arrays/InitVals.hs +++ b/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