more tests

LeventErkok · Sep 18, 2024 · f3c5642 · f3c5642
1 parent 805332c
commit f3c5642
Show file tree

Hide file tree

Showing 3 changed files with 78 additions and 11 deletions.
diff --git a/SBVTestSuite/GoldFiles/array_misc_7.gold b/SBVTestSuite/GoldFiles/array_misc_7.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_9.gold b/SBVTestSuite/GoldFiles/array_misc_9.gold
@@ -0,0 +1,27 @@
+** 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 ---
+[SEND] (check-sat)
+[RECV] sat
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Falsifiable
diff --git a/SBVTestSuite/TestSuite/Arrays/InitVals.hs b/SBVTestSuite/TestSuite/Arrays/InitVals.hs
@@ -66,22 +66,34 @@ tests = testGroup "Arrays" [
       , goldenCapturedIO "constArr2_SArray" $ t satWith constArr2
       ]
   , testGroup "Arrays.Misc"
-      [ goldenCapturedIO "array_misc_1" $ t proveWith $ \i -> readArray (listArray [(True,1),(False,0)] 3) i .<= (1::SInteger)
+      [ goldenCapturedIO "array_misc_1"  $ t proveWith $ \i -> readArray (listArray [(True,1),(False,0)] 3) i .<= (1::SInteger)
 
-      , goldenCapturedIO "array_misc_2" $ t satWith   $ \(x :: SArray Integer Integer) i1 i2 i3 ->
-                                                                readArray x i1 .== 4 .&& readArray x i2 .== 5 .&& readArray x i3 .== 12
+      , goldenCapturedIO "array_misc_2"  $ t satWith   $ \(x :: SArray Integer Integer) i1 i2 i3 ->
+                                                                 readArray x i1 .== 4 .&& readArray x i2 .== 5 .&& readArray x i3 .== 12
 
-      , goldenCapturedIO "array_misc_3" $ t proveWith $      write (empty False) [(True, True), (False, False)]
-                                                         .== write (empty True)  [(True, True), (False, False)]
+      , goldenCapturedIO "array_misc_3"  $ t proveWith $      write (empty False) [(True, True), (False, False)]
+                                                          .== write (empty True)  [(True, True), (False, False)]
 
-      , testCase         "array_misc_4" $                   (write (empty False) [(True, True), (False, False)]
-                                                         .== write (empty True)  [(True, True), (False, False)]) `showsAs` "True"
+      , testCase         "array_misc_4"  $                   (write (empty False) [(True, True), (False, False)]
+                                                          .== write (empty True)  [(True, True), (False, False)]) `showsAs` "True"
 
-      , goldenCapturedIO "array_misc_5" $ t proveWith $      write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
-                                                         .== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
+      , goldenCapturedIO "array_misc_5"  $ t proveWith $      write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
+                                                          .== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
 
-      , testCase         "array_misc_6" $                   (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
-                                                         .== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "<symbolic> :: SBool"
+      , testCase         "array_misc_6"  $                   (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
+                                                          .== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "<symbolic> :: SBool"
+
+      , goldenCapturedIO "array_misc_7"  $ t proveWith $      write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
+                                                          .== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
+
+      , testCase         "array_misc_8"  $                   (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
+                                                          .== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "True"
+
+      , goldenCapturedIO "array_misc_9"   $ t proveWith $     write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
+                                                          .== write (empty 0) [(i, i)   | i <- [0 .. (3 :: WordN 2)]]
+
+      , 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"
 
       ]
   ]