diff options
Diffstat (limited to 'test/regress/regress0/bug274.cvc.smt2')
| -rw-r--r-- | test/regress/regress0/bug274.cvc.smt2 | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test/regress/regress0/bug274.cvc.smt2 b/test/regress/regress0/bug274.cvc.smt2 new file mode 100644 index 000000000..035383601 --- /dev/null +++ b/test/regress/regress0/bug274.cvc.smt2 @@ -0,0 +1,33 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental true) +(declare-datatypes ((DT1 0)) (((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)))) +(declare-datatypes ((DT2 0)) (((DT2_a) (DT2_b) (DT2_c) (DT2_d)))) +(declare-datatypes ((DT3 0)) (((DT3_a) (DT3_b)))) +(declare-fun var1 () DT3) +(declare-fun var2 () DT3) +(declare-fun var3 () DT1) +(declare-fun var4 () DT3) +(declare-fun var5 () DT3) +(declare-fun var6 () DT3) +(declare-fun var7 () DT3) +(declare-fun var8 () DT3) +(declare-fun var9 () DT3) +(declare-fun var10 () DT3) +(declare-fun var11 () DT2) +(declare-fun var12 () DT3) +(declare-fun var13 () DT3) +(declare-fun var14 () DT3) +(declare-fun var16 () DT3) +(declare-fun var17 () DT3) +(declare-fun var18 () DT3) +(declare-fun var20 () DT3) +(declare-fun var21 () DT3) +(push 1) + +(assert (let ((_let_1 (or (or (and (and (= var7 DT3_b) (= var4 DT3_b)) (= var1 DT3_a)) (= (or (and (= var5 DT3_a) (= var17 DT3_b)) (and (= var21 DT3_b) (or (= var3 DT1_f) (= var3 DT1_g)))) (= DT3_b DT3_b))) (and (and (= var14 DT3_a) (= var2 DT3_a)) (or (or (or (and (= var8 DT3_a) (= var18 DT3_b)) (and (= var6 DT3_a) (not (= var11 DT2_a)))) (= var20 DT3_b)) (= var9 DT3_b)))))) (and (and (and (not (= var13 DT3_a)) (not (= var10 DT3_b))) (not (or _let_1 (and (not _let_1) (and (= var14 DT3_b) true))))) (not (or (= var12 DT3_a) (and (= var12 DT3_b) (or (= var16 DT3_b) true))))))) + +(check-sat) + +(pop 1) + |