diff --git a/SBVTestSuite/GoldFiles/array_misc_31.gold b/SBVTestSuite/GoldFiles/array_misc_31.gold new file mode 100644 index 000000000..460966a20 --- /dev/null +++ b/SBVTestSuite/GoldFiles/array_misc_31.gold @@ -0,0 +1,28 @@ +** 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 QF_BV) +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- tuples --- +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] ; --- top level inputs --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert false) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +Q.E.D. diff --git a/SBVTestSuite/GoldFiles/array_misc_32.gold b/SBVTestSuite/GoldFiles/array_misc_32.gold new file mode 100644 index 000000000..f718b3799 --- /dev/null +++ b/SBVTestSuite/GoldFiles/array_misc_32.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-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] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0)))) +[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0)))) +[GOOD] ; --- top level inputs --- +[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 (not s2)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +Q.E.D. diff --git a/SBVTestSuite/GoldFiles/array_misc_33.gold b/SBVTestSuite/GoldFiles/array_misc_33.gold new file mode 100644 index 000000000..44935e025 --- /dev/null +++ b/SBVTestSuite/GoldFiles/array_misc_33.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-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] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0)))) +[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0)))) +[GOOD] ; --- top level inputs --- +[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 (not s2)) +[SEND] (check-sat) +[RECV] sat +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +Falsifiable diff --git a/SBVTestSuite/GoldFiles/array_misc_34.gold b/SBVTestSuite/GoldFiles/array_misc_34.gold new file mode 100644 index 000000000..f8de695db --- /dev/null +++ b/SBVTestSuite/GoldFiles/array_misc_34.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-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] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0)))) +[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0)))) +[GOOD] ; --- top level inputs --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s2 () Bool (distinct s0 s1)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s2)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +Q.E.D. diff --git a/SBVTestSuite/TestSuite/Arrays/InitVals.hs b/SBVTestSuite/TestSuite/Arrays/InitVals.hs index f94bab533..44178dac4 100644 --- a/SBVTestSuite/TestSuite/Arrays/InitVals.hs +++ b/SBVTestSuite/TestSuite/Arrays/InitVals.hs @@ -122,6 +122,11 @@ tests = testGroup "Arrays" [ , 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)) + + , goldenCapturedIO "array_misc_31" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Integer)) + , goldenCapturedIO "array_misc_32" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double)) + , goldenCapturedIO "array_misc_33" $ t proveWith (listArray [(1, 2), (3, 1)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double)) + , goldenCapturedIO "array_misc_34" $ t proveWith (listArray [(1, 2), (3, 1)] 5 ./= listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double)) ] ] where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f