; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic BV)

;Trace length 
(define-sort Stream () (_ BitVec 48))
(define-fun ZERO () Stream (_ bv0 48))
(define-fun ONE () Stream (_ bv1 48))


(define-fun S_FALSE () Stream ZERO)
(define-fun S_TRUE () Stream (bvnot S_FALSE))

; Yesterday: X << 1
(define-fun
  Y ( (X Stream) ) Stream
  (bvshl X ONE)
)

; Once: X|-X
(define-fun
  O ( (X Stream) ) Stream
  (bvor X (bvneg X))
)

; Historically: X & ~(1 + X)
(define-fun
  H ( (X Stream) ) Stream
  (bvand X (bvnot (bvadd ONE X)))
)

; Since: Z | (X & ~((X | Z) + Z))
(define-fun
S ( (X Stream) (Z Stream) ) Stream
  (bvor Z
    (bvand X 
      (bvnot (bvadd  (bvor X Z) Z ))
    )
  )
)

(define-fun
  bvimpl ( (X Stream) (Z Stream) ) Stream
  (bvor (bvnot X) Z)
)

(synth-fun phi ((ulInformationTransfer Stream) (dlInformationTransfer Stream) (rrcConnectionReconfiguration Stream) (measurementReport Stream) (systemInformationBlockType1 Stream) (securityModeComplete Stream) (systemInformation Stream) (rrcConnectionReestablishmentReject Stream) (rrcConnectionRequest Stream) (rrcConnectionSetupComplete Stream) (rrcConnectionRelease Stream) (ueCapabilityInformation Stream) (rrcConnectionSetup Stream) (securityModeCommand Stream) (ueCapabilityEnquiry Stream) (rrcConnectionReconfigurationComplete Stream) (rrcConnectionReestablishmentRequest Stream)) Stream
   ((<F> Stream))
   ((<F> Stream (
     S_TRUE 
     S_FALSE
     ( Variable Stream ) 
     (bvnot <F>)
     (bvand <F> <F>) 
     (bvor <F> <F>)
     (bvimpl <F> <F>)
     (Y <F>)
     (O <F>)
     (H <F>)
     (S <F> <F>)
   )))
)

;; Positive examples
;Positive Trace Data
(constraint
   (and
    (= ((_ extract 8 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000011000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 8 0) S_TRUE))
    (= (phi #b000000000000000000000100000000100000000000000000 #b000000000000000000000010000000000000000000000000 #b000000101000000001010000000100000100001000100000 #b000000000100000000001000000000000010100000000000 #b000010000001000100000001000000010000000000000000 #b000000000000000000000000000000000000000000010000 #b001100000010111000000000110011000001000000000000 #b100000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000010000000 #b000001010000000010100000001000001000010001000000 #b010000000000000000000000000000000000000000000000) S_TRUE)
    (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010000010100000 #b000000000000000000000000000000000001100000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000010000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000100000101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
    (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000010001000000 #b000000000000000000000000000000000111000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000100010000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
    (= ((_ extract 20 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000001001001010100000 #b000000000000000000000000000000000000100000000000 #b000000000000000000000000000010000100000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000001100000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000100000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000010010010101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 20 0) S_TRUE)) 
   )
)

;; Negative examples

;Negative Trace Data
(constraint
   (and
    (not (= ((_ extract 6 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000110000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 6 0) S_TRUE)))
    (not (= ((_ extract 45 0) (phi #b000000000000000000000001000000001000000000000000 #b000000000000000000000000100000000000000000000000 #b000000001010000000010100000001000001000010001000 #b000000000001000000000010000000000000101000000000 #b000000100000010001000000010000000100000000000000 #b000000000000000000000000000000000000000000000000 #b000011000000101110000000001100110000010000000000 #b001000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000010100000000101000000010000010000100010000 #b000100000000000000000000000000000000000000000000)) ((_ extract 45 0) S_TRUE)))
    (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000100000101000 #b000000000000000000000000000000000000011000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000001000001010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
    (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100010000 #b000000000000000000000000000000000001110000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000001000100000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
    (not (= ((_ extract 18 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010010010101000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000100001000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000011000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000001000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000100100101010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 18 0) S_TRUE))) 
   )
)

; Solution: G (p -> O f) 
(check-synth)