error asserting datatype of datatype in z3

Question

I've this problem:

(set-option :print-success true)
(declare-datatypes () (( Data nil (cons (giorno Int) (mese Int)(anno Int) ))))
(declare-datatypes () (( Eta  (cons1  (data Data) (io Int)))))
(assert (forall ( (e Eta) )
(and (< 0 ((giorno data) e)) (> 0 ((giorno data) e))
) ) )
(check-sat)

and z3 return me this:

Z3(7, 12): ERROR: invalid qualified/indexed identifier, '_' or 'as' expected

how can i resolve this?

Answer 1

I think that the correct code is

(set-option :print-success true)
(declare-datatypes () (( Data nil (cons (giorno Int) (mese Int)(anno Int) ))))
(declare-datatypes () (( Eta  (cons1  (data Data) (io Int)))))
(assert (forall ( (e Eta) )
(and (< 0 (giorno (data e))) (> 0 (giorno (data e))))))
(check-sat)

and the output is

success 
success 
success 
success 
unsat