summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug274.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/bug274.cvc')
-rw-r--r--test/regress/regress0/bug274.cvc64
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)))))
-);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback