
Hello all,
I am trying to define a record datatype in z3 consisting of six elements of different types. This is how I did it: (declaredatatypes () ((S (mkpair (p1 (P1type)) (p2 (P2type)) (p3 (P3type)) (m1 (bool)) (m2 (bool)) (m3 (bool)) )))) But when I use (forall (x1
S)), the solver does not seem to consider all possible combinations of valuations for my datatype. I appreciate if you let me know if I am doing something wrong, or I should not expect z3 to consider all combinations of valuations for S.
Thanks a lot,
Fathiyeh



I think I resolved my issue :)

