test/regress/regress0/bug274.cvc

   1 % EXPECT: unsat
   2 DATATYPE DT1 =
   3   DT1_a |
   4   DT1_b |
   5   DT1_c |
   6   DT1_d |
   7   DT1_e |
   8   DT1_f |
   9   DT1_g |
  10   DT1_h |
  11   DT1_i |
  12   DT1_j |
  13   DT1_k |
  14   DT1_l |
  15   DT1_m |
  16   DT1_n |
  17   DT1_o |
  18   DT1_p |
  19   DT1_q |
  20   DT1_r |
  21   DT1_s |
  22   DT1_t |
  23   DT1_u |
  24   DT1_v |
  25   DT1_w |
  26   DT1_x |
  27   DT1_y |
  28   DT1_z
  29 END;
  30 DATATYPE DT2 =
  31   DT2_a |
  32   DT2_b |
  33   DT2_c |
  34   DT2_d
  35 END;
  36 DATATYPE DT3 =
  37   DT3_a |
  38   DT3_b
  39 END;
  40 var1 : DT3;
  41 var2 : DT3;
  42 var3 : DT1;
  43 var4 : DT3;
  44 var5 : DT3;
  45 var6 : DT3;
  46 var7 : DT3;
  47 var8 : DT3;
  48 var9 : DT3;
  49 var10 : DT3;
  50 var11 : DT2;
  51 var12 : DT3;
  52 var13 : DT3;
  53 var14 : DT3;
  54 var16 : DT3;
  55 var17 : DT3;
  56 var18 : DT3;
  57 var20 : DT3;
  58 var21 : DT3;
  59 CHECKSAT
  60 (
  61         (((NOT(var13 = DT3_a)) AND (NOT(var10 = DT3_b))) AND (NOT((((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b)))) OR ((NOT(((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b))))) AND ((var14 = DT3_b) AND (TRUE))))))
  62     AND
  63         (NOT((var12 = DT3_a) OR ((var12 = DT3_b) AND ((var16 = DT3_b) OR (TRUE)))))
  64 );