diff options
Diffstat (limited to 'test/regress/regress0/bug274.cvc')
-rw-r--r-- | test/regress/regress0/bug274.cvc | 64 |
1 files changed, 0 insertions, 64 deletions
diff --git a/test/regress/regress0/bug274.cvc b/test/regress/regress0/bug274.cvc deleted file mode 100644 index c30f95550..000000000 --- a/test/regress/regress0/bug274.cvc +++ /dev/null @@ -1,64 +0,0 @@ -% EXPECT: unsat -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))))) -); |