All possible values for a record datatype in Z3?

Aug 20, 2013 at 5:19 PM
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: (declare-datatypes () ((S (mk-pair (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
Aug 21, 2013 at 5:12 PM
I think I resolved my issue :-)