; Query 1 -- Type: InitialValues, Instructions: 11656
(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun input () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (=  (_ bv5 32) (bvurem  (bvadd  (_ bv4 32) (bvudiv  (concat  (select  input (_ bv3 32) ) (concat  (select  input (_ bv2 32) ) (concat  (select  input (_ bv1 32) ) (select  input (_ bv0 32) ) ) ) ) (_ bv86400 32) ) ) (_ bv7 32) ) ) )
(check-sat)
(get-value ( (select input (_ bv0 32) ) ) )
(get-value ( (select input (_ bv1 32) ) ) )
(get-value ( (select input (_ bv2 32) ) ) )
(get-value ( (select input (_ bv3 32) ) ) )
(exit)
;   OK -- Elapsed: 2.303087e-02s
;   Solvable: true
;     input = [128,81,1,0]

; Query 2 -- Type: InitialValues, Instructions: 11676
(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun input () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (concat  (select  input (_ bv3 32) ) (concat  (select  input (_ bv2 32) ) (concat  (select  input (_ bv1 32) ) (select  input (_ bv0 32) ) ) ) ) ) ) (and  (bvult  (_ bv64799 32) (bvurem  ?B1 (_ bv86400 32) ) ) (=  (_ bv5 32) (bvurem  (bvadd  (_ bv4 32) (bvudiv  ?B1 (_ bv86400 32) ) ) (_ bv7 32) ) ) ) ) )
(check-sat)
(get-value ( (select input (_ bv0 32) ) ) )
(get-value ( (select input (_ bv1 32) ) ) )
(get-value ( (select input (_ bv2 32) ) ) )
(get-value ( (select input (_ bv3 32) ) ) )
(exit)
;   OK -- Elapsed: 2.374635e-02s
;   Solvable: true
;     input = [0,112,2,0]