Z3 issue #1922

ex1.smt2

;; ex1.smt2
(get-info :version)

; A tuple of two booleans
; data Tuple = tuple { first :: Bool, second :: Bool }
(declare-datatypes
  ((Tuple 0))
  ((Tuple (tuple
    (first  Bool)
    (second Bool)
))))


; Option type of a tuple
; data Option = none | some { value :: Tuple }}
(declare-datatypes ((Option 0)) ((Option (none) (some (value Tuple)))))

; x :: Option is a constant
(declare-fun x () Option)

; Assertion 1. x has some value
(assert ((_ is (some (Tuple) Option)) x))

; Assertion 2. first (value x) == true
(assert (first (value x)))

(check-sat)
(get-model)

(echo "(first (value x)) = ")
(eval (first (value x)))

ex2.smt2

;; ex2.smt2
(get-info :version)

; A tuple of two booleans and one integer
; data Tuple = tuple { first :: Bool, second :: Bool, third :: Int }
(declare-datatypes
  ((Tuple 0))
  ((Tuple (tuple
    (first  Bool)
    (second Bool)
    (third  Int)  ; new field
))))

; same as ex1.smt2 ...

; Option type of a tuple
; data Option = none | some { value :: Tuple }}
(declare-datatypes ((Option 0)) ((Option (none) (some (value Tuple)))))

; x :: Option is a constant
(declare-fun x () Option)

; Assertion 1. x has some value
(assert ((_ is (some (Tuple) Option)) x))

; Assertion 2. first (value x) == b10
(assert (first (value x)))

(check-sat)
(get-model)

(echo "(first (value x)) = ")
(eval (first (value x)))

ex3.smt2

;; ex3.smt2
(get-info :version)

; A tuple of two booleans
; data Tuple = tuple { first :: Bool, second :: Bool }
(declare-datatypes
  () ; ((Tuple 0))
  ((Tuple (tuple
    (first  Bool)
    (second Bool)
))))

; same as ex1.smt2 ...

; Option type of a tuple
; data Option = none | some { value :: Tuple }}
(declare-datatypes ((Option 0)) ((Option (none) (some (value Tuple)))))

; x :: Option is a constant
(declare-fun x () Option)

; Assertion 1. x has some value
(assert ((_ is (some (Tuple) Option)) x))

; Assertion 2. first (value x) == true
(assert (first (value x)))

(check-sat)
(get-model)

(echo "(first (value x)) = ")
(eval (first (value x)))