diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 05:27:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 05:27:33 +0000 |
commit | 8116fa6b55db64301ed89f1f174b95780449007f (patch) | |
tree | f75566f83d9bbefd9fd5cb2b34feab7d7a3faa84 /test/regress/regress0/bug274.cvc | |
parent | 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 (diff) |
* Include a few bug testcases for resolved bugs.
* Fix error message if you POP beyond the bottom user stack frame.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test/regress/regress0/bug274.cvc')
-rw-r--r-- | test/regress/regress0/bug274.cvc | 65 |
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))))) +); |