Test cases for #374

SBVTestSuite/GoldFiles/queryArrays6.gold

@@ -0,0 +1,79 @@
+** 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 non-bitvector arrays, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s_2 () Bool false)
+[GOOD] (define-fun s_1 () Bool true)
+[GOOD] ; --- skolem constants ---
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- skolemized tables ---
+[GOOD] ; --- arrays ---
+[GOOD] (declare-fun array_0 () (Array Int Int))
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user given axioms ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s_1)
+[GOOD] (push 1)
+[GOOD] (define-fun s0 () Int 1)
+[GOOD] (define-fun s2 () Int 5)
+[GOOD] (declare-fun array_1 () (Array Int Int))
+[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s0)))
+[GOOD] (define-fun s1 () Int (select array_1 s0))
+[GOOD] (define-fun s3 () Bool (= s1 s2))
+[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
+[GOOD] (assert array_1_initializer)
+[GOOD] (assert s3)
+[SEND] (check-sat)
+[RECV] unsat
+[GOOD] (pop 1)
+[GOOD] (assert array_1_initializer)
+[GOOD] (declare-fun s4 () Int)
+[GOOD] (define-fun s6 () Int 3)
+[GOOD] (define-fun s5 () Bool (>= s4 s0))
+[GOOD] (define-fun s7 () Bool (< s4 s6))
+[GOOD] (define-fun s8 () Bool (and s5 s7))
+[GOOD] (assert s8)
+[GOOD] (push 1)
+[GOOD] (declare-fun array_2 () (Array Int Int))
+[GOOD] (define-fun s9 () Int (+ s1 s4))
+[GOOD] (define-fun s10 () Int (select array_2 s0))
+[GOOD] (define-fun s11 () Bool (= s2 s10))
+[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s0 s9)))
+[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)
+[GOOD] (assert array_2_initializer)
+[GOOD] (assert s11)
+[SEND] (check-sat)
+[RECV] unsat
+[GOOD] (pop 1)
+[GOOD] (assert (and array_1_initializer array_2_initializer))
+[GOOD] (declare-fun s12 () Int)
+[GOOD] (define-fun s13 () Bool (>= s12 s0))
+[GOOD] (define-fun s14 () Bool (< s12 s6))
+[GOOD] (define-fun s15 () Bool (and s13 s14))
+[GOOD] (assert s15)
+[GOOD] (push 1)
+[GOOD] (declare-fun array_3 () (Array Int Int))
+[GOOD] (define-fun s16 () Int (+ s10 s12))
+[GOOD] (define-fun s17 () Int (select array_3 s0))
+[GOOD] (define-fun s18 () Bool (= s2 s17))
+[GOOD] (define-fun array_3_initializer_0 () Bool (= array_3 (store array_2 s0 s16)))
+[GOOD] (define-fun array_3_initializer () Bool array_3_initializer_0)
+[GOOD] (assert array_3_initializer)
+[GOOD] (assert s18)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s4))
+[RECV] ((s4 2))
+[SEND] (get-value (s12))
+[RECV] ((s12 2))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+ FINAL:[2,2]
+DONE!

SBVTestSuite/TestSuite/Arrays/Query.hs

@@ -26,6 +26,7 @@ tests =
     , goldenCapturedIO "queryArrays3" $ t q3
     , goldenCapturedIO "queryArrays4" $ t q4
     , goldenCapturedIO "queryArrays5" $ t q5
+    , goldenCapturedIO "queryArrays6" $ t q6
     ]
     where t tc goldFile = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc
                              appendFile goldFile ("\n FINAL:" ++ show r ++ "\nDONE!\n")
@@ -100,4 +101,20 @@ q5 = do m  :: SArray Word8 Int8 <- newArray "a"
                                  vv <- getValue v
                                  return $ Just (av, vv)
 
+q6 :: Symbolic [Integer]
+q6 = do (a :: SArray Integer Integer) <- newArray "a"
+
+        query $ loop (writeArray a 1 1) []
+
+  where loop a sofar = do push 1
+                          constrain $ readArray a 1 .== 5
+                          cs <- checkSat
+                          case cs of
+                            Unk   -> error "Unknown"
+                            Unsat -> do pop 1
+                                        d <- freshVar $ "d" ++ show (length sofar)
+                                        constrain $ d .>= 1 &&& d .< 3
+                                        loop (writeArray a 1 (readArray a 1 + d)) (sofar ++ [d])
+                            Sat   -> mapM getValue sofar
+
 {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}