1 files changed, 65 insertions, 0 deletions
diff --git a/test/regress/regress0/bug274.cvc b/test/regress/regress0/bug274.cvc
new file mode 100644
index 000000000..7b3df50d8
--- /dev/null
+++ b/test/regress/regress0/bug274.cvc
@@ -0,0 +1,65 @@
+% EXPECT: unsat
+% EXIT: 20
+DATATYPE DT1 = 
+  DT1_a |
+  DT1_b |
+  DT1_c |
+  DT1_d |
+  DT1_e |
+  DT1_f |
+  DT1_g |
+  DT1_h |
+  DT1_i |
+  DT1_j |
+  DT1_k |
+  DT1_l |
+  DT1_m |
+  DT1_n |
+  DT1_o |
+  DT1_p |
+  DT1_q |
+  DT1_r |
+  DT1_s |
+  DT1_t |
+  DT1_u |
+  DT1_v |
+  DT1_w |
+  DT1_x |
+  DT1_y |
+  DT1_z
+END;
+DATATYPE DT2 = 
+  DT2_a |
+  DT2_b |
+  DT2_c |
+  DT2_d
+END;
+DATATYPE DT3 = 
+  DT3_a |
+  DT3_b
+END;
+var1 : DT3;
+var2 : DT3;
+var3 : DT1;
+var4 : DT3;
+var5 : DT3;
+var6 : DT3;
+var7 : DT3;
+var8 : DT3;
+var9 : DT3;
+var10 : DT3;
+var11 : DT2;
+var12 : DT3;
+var13 : DT3;
+var14 : DT3;
+var16 : DT3;
+var17 : DT3;
+var18 : DT3;
+var20 : DT3;
+var21 : DT3;
+CHECKSAT
+(
+        (((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))))))
+    AND
+        (NOT((var12 = DT3_a) OR ((var12 = DT3_b) AND ((var16 = DT3_b) OR (TRUE)))))
+);