diff options
Diffstat (limited to 'test/regress/regress1/hole6.cvc.smt2')
| -rw-r--r-- | test/regress/regress1/hole6.cvc.smt2 | 180 |
1 files changed, 180 insertions, 0 deletions
diff --git a/test/regress/regress1/hole6.cvc.smt2 b/test/regress/regress1/hole6.cvc.smt2 new file mode 100644 index 000000000..80dc40617 --- /dev/null +++ b/test/regress/regress1/hole6.cvc.smt2 @@ -0,0 +1,180 @@ +; COMMAND-LINE: --no-check-proofs +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x_1 () Bool) +(declare-fun x_2 () Bool) +(declare-fun x_3 () Bool) +(declare-fun x_4 () Bool) +(declare-fun x_5 () Bool) +(declare-fun x_6 () Bool) +(declare-fun x_7 () Bool) +(declare-fun x_8 () Bool) +(declare-fun x_9 () Bool) +(declare-fun x_10 () Bool) +(declare-fun x_11 () Bool) +(declare-fun x_12 () Bool) +(declare-fun x_13 () Bool) +(declare-fun x_14 () Bool) +(declare-fun x_15 () Bool) +(declare-fun x_16 () Bool) +(declare-fun x_17 () Bool) +(declare-fun x_18 () Bool) +(declare-fun x_19 () Bool) +(declare-fun x_20 () Bool) +(declare-fun x_21 () Bool) +(declare-fun x_22 () Bool) +(declare-fun x_23 () Bool) +(declare-fun x_24 () Bool) +(declare-fun x_25 () Bool) +(declare-fun x_26 () Bool) +(declare-fun x_27 () Bool) +(declare-fun x_28 () Bool) +(declare-fun x_29 () Bool) +(declare-fun x_30 () Bool) +(declare-fun x_31 () Bool) +(declare-fun x_32 () Bool) +(declare-fun x_33 () Bool) +(declare-fun x_34 () Bool) +(declare-fun x_35 () Bool) +(declare-fun x_36 () Bool) +(declare-fun x_37 () Bool) +(declare-fun x_38 () Bool) +(declare-fun x_39 () Bool) +(declare-fun x_40 () Bool) +(declare-fun x_41 () Bool) +(declare-fun x_42 () Bool) +(assert (or (not x_1) (not x_7))) +(assert (or (not x_1) (not x_13))) +(assert (or (not x_1) (not x_19))) +(assert (or (not x_1) (not x_25))) +(assert (or (not x_1) (not x_31))) +(assert (or (not x_1) (not x_37))) +(assert (or (not x_7) (not x_13))) +(assert (or (not x_7) (not x_19))) +(assert (or (not x_7) (not x_25))) +(assert (or (not x_7) (not x_31))) +(assert (or (not x_7) (not x_37))) +(assert (or (not x_13) (not x_19))) +(assert (or (not x_13) (not x_25))) +(assert (or (not x_13) (not x_31))) +(assert (or (not x_13) (not x_37))) +(assert (or (not x_19) (not x_25))) +(assert (or (not x_19) (not x_31))) +(assert (or (not x_19) (not x_37))) +(assert (or (not x_25) (not x_31))) +(assert (or (not x_25) (not x_37))) +(assert (or (not x_31) (not x_37))) +(assert (or (not x_2) (not x_8))) +(assert (or (not x_2) (not x_14))) +(assert (or (not x_2) (not x_20))) +(assert (or (not x_2) (not x_26))) +(assert (or (not x_2) (not x_32))) +(assert (or (not x_2) (not x_38))) +(assert (or (not x_8) (not x_14))) +(assert (or (not x_8) (not x_20))) +(assert (or (not x_8) (not x_26))) +(assert (or (not x_8) (not x_32))) +(assert (or (not x_8) (not x_38))) +(assert (or (not x_14) (not x_20))) +(assert (or (not x_14) (not x_26))) +(assert (or (not x_14) (not x_32))) +(assert (or (not x_14) (not x_38))) +(assert (or (not x_20) (not x_26))) +(assert (or (not x_20) (not x_32))) +(assert (or (not x_20) (not x_38))) +(assert (or (not x_26) (not x_32))) +(assert (or (not x_26) (not x_38))) +(assert (or (not x_32) (not x_38))) +(assert (or (not x_3) (not x_9))) +(assert (or (not x_3) (not x_15))) +(assert (or (not x_3) (not x_21))) +(assert (or (not x_3) (not x_27))) +(assert (or (not x_3) (not x_33))) +(assert (or (not x_3) (not x_39))) +(assert (or (not x_9) (not x_15))) +(assert (or (not x_9) (not x_21))) +(assert (or (not x_9) (not x_27))) +(assert (or (not x_9) (not x_33))) +(assert (or (not x_9) (not x_39))) +(assert (or (not x_15) (not x_21))) +(assert (or (not x_15) (not x_27))) +(assert (or (not x_15) (not x_33))) +(assert (or (not x_15) (not x_39))) +(assert (or (not x_21) (not x_27))) +(assert (or (not x_21) (not x_33))) +(assert (or (not x_21) (not x_39))) +(assert (or (not x_27) (not x_33))) +(assert (or (not x_27) (not x_39))) +(assert (or (not x_33) (not x_39))) +(assert (or (not x_4) (not x_10))) +(assert (or (not x_4) (not x_16))) +(assert (or (not x_4) (not x_22))) +(assert (or (not x_4) (not x_28))) +(assert (or (not x_4) (not x_34))) +(assert (or (not x_4) (not x_40))) +(assert (or (not x_10) (not x_16))) +(assert (or (not x_10) (not x_22))) +(assert (or (not x_10) (not x_28))) +(assert (or (not x_10) (not x_34))) +(assert (or (not x_10) (not x_40))) +(assert (or (not x_16) (not x_22))) +(assert (or (not x_16) (not x_28))) +(assert (or (not x_16) (not x_34))) +(assert (or (not x_16) (not x_40))) +(assert (or (not x_22) (not x_28))) +(assert (or (not x_22) (not x_34))) +(assert (or (not x_22) (not x_40))) +(assert (or (not x_28) (not x_34))) +(assert (or (not x_28) (not x_40))) +(assert (or (not x_34) (not x_40))) +(assert (or (not x_5) (not x_11))) +(assert (or (not x_5) (not x_17))) +(assert (or (not x_5) (not x_23))) +(assert (or (not x_5) (not x_29))) +(assert (or (not x_5) (not x_35))) +(assert (or (not x_5) (not x_41))) +(assert (or (not x_11) (not x_17))) +(assert (or (not x_11) (not x_23))) +(assert (or (not x_11) (not x_29))) +(assert (or (not x_11) (not x_35))) +(assert (or (not x_11) (not x_41))) +(assert (or (not x_17) (not x_23))) +(assert (or (not x_17) (not x_29))) +(assert (or (not x_17) (not x_35))) +(assert (or (not x_17) (not x_41))) +(assert (or (not x_23) (not x_29))) +(assert (or (not x_23) (not x_35))) +(assert (or (not x_23) (not x_41))) +(assert (or (not x_29) (not x_35))) +(assert (or (not x_29) (not x_41))) +(assert (or (not x_35) (not x_41))) +(assert (or (not x_6) (not x_12))) +(assert (or (not x_6) (not x_18))) +(assert (or (not x_6) (not x_24))) +(assert (or (not x_6) (not x_30))) +(assert (or (not x_6) (not x_36))) +(assert (or (not x_6) (not x_42))) +(assert (or (not x_12) (not x_18))) +(assert (or (not x_12) (not x_24))) +(assert (or (not x_12) (not x_30))) +(assert (or (not x_12) (not x_36))) +(assert (or (not x_12) (not x_42))) +(assert (or (not x_18) (not x_24))) +(assert (or (not x_18) (not x_30))) +(assert (or (not x_18) (not x_36))) +(assert (or (not x_18) (not x_42))) +(assert (or (not x_24) (not x_30))) +(assert (or (not x_24) (not x_36))) +(assert (or (not x_24) (not x_42))) +(assert (or (not x_30) (not x_36))) +(assert (or (not x_30) (not x_42))) +(assert (or (not x_36) (not x_42))) +(assert (or (or (or (or (or x_6 x_5) x_4) x_3) x_2) x_1)) +(assert (or (or (or (or (or x_12 x_11) x_10) x_9) x_8) x_7)) +(assert (or (or (or (or (or x_18 x_17) x_16) x_15) x_14) x_13)) +(assert (or (or (or (or (or x_24 x_23) x_22) x_21) x_20) x_19)) +(assert (or (or (or (or (or x_30 x_29) x_28) x_27) x_26) x_25)) +(assert (or (or (or (or (or x_36 x_35) x_34) x_33) x_32) x_31)) +(assert (or (or (or (or (or x_42 x_41) x_40) x_39) x_38) x_37)) +(check-sat) |