diff options
Diffstat (limited to 'test/regress/regress3/hole9.cvc.smt2')
| -rw-r--r-- | test/regress/regress3/hole9.cvc.smt2 | 509 |
1 files changed, 509 insertions, 0 deletions
diff --git a/test/regress/regress3/hole9.cvc.smt2 b/test/regress/regress3/hole9.cvc.smt2 new file mode 100644 index 000000000..c62eab886 --- /dev/null +++ b/test/regress/regress3/hole9.cvc.smt2 @@ -0,0 +1,509 @@ +; 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) +(declare-fun x_43 () Bool) +(declare-fun x_44 () Bool) +(declare-fun x_45 () Bool) +(declare-fun x_46 () Bool) +(declare-fun x_47 () Bool) +(declare-fun x_48 () Bool) +(declare-fun x_49 () Bool) +(declare-fun x_50 () Bool) +(declare-fun x_51 () Bool) +(declare-fun x_52 () Bool) +(declare-fun x_53 () Bool) +(declare-fun x_54 () Bool) +(declare-fun x_55 () Bool) +(declare-fun x_56 () Bool) +(declare-fun x_57 () Bool) +(declare-fun x_58 () Bool) +(declare-fun x_59 () Bool) +(declare-fun x_60 () Bool) +(declare-fun x_61 () Bool) +(declare-fun x_62 () Bool) +(declare-fun x_63 () Bool) +(declare-fun x_64 () Bool) +(declare-fun x_65 () Bool) +(declare-fun x_66 () Bool) +(declare-fun x_67 () Bool) +(declare-fun x_68 () Bool) +(declare-fun x_69 () Bool) +(declare-fun x_70 () Bool) +(declare-fun x_71 () Bool) +(declare-fun x_72 () Bool) +(declare-fun x_73 () Bool) +(declare-fun x_74 () Bool) +(declare-fun x_75 () Bool) +(declare-fun x_76 () Bool) +(declare-fun x_77 () Bool) +(declare-fun x_78 () Bool) +(declare-fun x_79 () Bool) +(declare-fun x_80 () Bool) +(declare-fun x_81 () Bool) +(declare-fun x_82 () Bool) +(declare-fun x_83 () Bool) +(declare-fun x_84 () Bool) +(declare-fun x_85 () Bool) +(declare-fun x_86 () Bool) +(declare-fun x_87 () Bool) +(declare-fun x_88 () Bool) +(declare-fun x_89 () Bool) +(declare-fun x_90 () Bool) +(assert (or (not x_1) (not x_10))) +(assert (or (not x_1) (not x_19))) +(assert (or (not x_1) (not x_28))) +(assert (or (not x_1) (not x_37))) +(assert (or (not x_1) (not x_46))) +(assert (or (not x_1) (not x_55))) +(assert (or (not x_1) (not x_64))) +(assert (or (not x_1) (not x_73))) +(assert (or (not x_1) (not x_82))) +(assert (or (not x_10) (not x_19))) +(assert (or (not x_10) (not x_28))) +(assert (or (not x_10) (not x_37))) +(assert (or (not x_10) (not x_46))) +(assert (or (not x_10) (not x_55))) +(assert (or (not x_10) (not x_64))) +(assert (or (not x_10) (not x_73))) +(assert (or (not x_10) (not x_82))) +(assert (or (not x_19) (not x_28))) +(assert (or (not x_19) (not x_37))) +(assert (or (not x_19) (not x_46))) +(assert (or (not x_19) (not x_55))) +(assert (or (not x_19) (not x_64))) +(assert (or (not x_19) (not x_73))) +(assert (or (not x_19) (not x_82))) +(assert (or (not x_28) (not x_37))) +(assert (or (not x_28) (not x_46))) +(assert (or (not x_28) (not x_55))) +(assert (or (not x_28) (not x_64))) +(assert (or (not x_28) (not x_73))) +(assert (or (not x_28) (not x_82))) +(assert (or (not x_37) (not x_46))) +(assert (or (not x_37) (not x_55))) +(assert (or (not x_37) (not x_64))) +(assert (or (not x_37) (not x_73))) +(assert (or (not x_37) (not x_82))) +(assert (or (not x_46) (not x_55))) +(assert (or (not x_46) (not x_64))) +(assert (or (not x_46) (not x_73))) +(assert (or (not x_46) (not x_82))) +(assert (or (not x_55) (not x_64))) +(assert (or (not x_55) (not x_73))) +(assert (or (not x_55) (not x_82))) +(assert (or (not x_64) (not x_73))) +(assert (or (not x_64) (not x_82))) +(assert (or (not x_73) (not x_82))) +(assert (or (not x_2) (not x_11))) +(assert (or (not x_2) (not x_20))) +(assert (or (not x_2) (not x_29))) +(assert (or (not x_2) (not x_38))) +(assert (or (not x_2) (not x_47))) +(assert (or (not x_2) (not x_56))) +(assert (or (not x_2) (not x_65))) +(assert (or (not x_2) (not x_74))) +(assert (or (not x_2) (not x_83))) +(assert (or (not x_11) (not x_20))) +(assert (or (not x_11) (not x_29))) +(assert (or (not x_11) (not x_38))) +(assert (or (not x_11) (not x_47))) +(assert (or (not x_11) (not x_56))) +(assert (or (not x_11) (not x_65))) +(assert (or (not x_11) (not x_74))) +(assert (or (not x_11) (not x_83))) +(assert (or (not x_20) (not x_29))) +(assert (or (not x_20) (not x_38))) +(assert (or (not x_20) (not x_47))) +(assert (or (not x_20) (not x_56))) +(assert (or (not x_20) (not x_65))) +(assert (or (not x_20) (not x_74))) +(assert (or (not x_20) (not x_83))) +(assert (or (not x_29) (not x_38))) +(assert (or (not x_29) (not x_47))) +(assert (or (not x_29) (not x_56))) +(assert (or (not x_29) (not x_65))) +(assert (or (not x_29) (not x_74))) +(assert (or (not x_29) (not x_83))) +(assert (or (not x_38) (not x_47))) +(assert (or (not x_38) (not x_56))) +(assert (or (not x_38) (not x_65))) +(assert (or (not x_38) (not x_74))) +(assert (or (not x_38) (not x_83))) +(assert (or (not x_47) (not x_56))) +(assert (or (not x_47) (not x_65))) +(assert (or (not x_47) (not x_74))) +(assert (or (not x_47) (not x_83))) +(assert (or (not x_56) (not x_65))) +(assert (or (not x_56) (not x_74))) +(assert (or (not x_56) (not x_83))) +(assert (or (not x_65) (not x_74))) +(assert (or (not x_65) (not x_83))) +(assert (or (not x_74) (not x_83))) +(assert (or (not x_3) (not x_12))) +(assert (or (not x_3) (not x_21))) +(assert (or (not x_3) (not x_30))) +(assert (or (not x_3) (not x_39))) +(assert (or (not x_3) (not x_48))) +(assert (or (not x_3) (not x_57))) +(assert (or (not x_3) (not x_66))) +(assert (or (not x_3) (not x_75))) +(assert (or (not x_3) (not x_84))) +(assert (or (not x_12) (not x_21))) +(assert (or (not x_12) (not x_30))) +(assert (or (not x_12) (not x_39))) +(assert (or (not x_12) (not x_48))) +(assert (or (not x_12) (not x_57))) +(assert (or (not x_12) (not x_66))) +(assert (or (not x_12) (not x_75))) +(assert (or (not x_12) (not x_84))) +(assert (or (not x_21) (not x_30))) +(assert (or (not x_21) (not x_39))) +(assert (or (not x_21) (not x_48))) +(assert (or (not x_21) (not x_57))) +(assert (or (not x_21) (not x_66))) +(assert (or (not x_21) (not x_75))) +(assert (or (not x_21) (not x_84))) +(assert (or (not x_30) (not x_39))) +(assert (or (not x_30) (not x_48))) +(assert (or (not x_30) (not x_57))) +(assert (or (not x_30) (not x_66))) +(assert (or (not x_30) (not x_75))) +(assert (or (not x_30) (not x_84))) +(assert (or (not x_39) (not x_48))) +(assert (or (not x_39) (not x_57))) +(assert (or (not x_39) (not x_66))) +(assert (or (not x_39) (not x_75))) +(assert (or (not x_39) (not x_84))) +(assert (or (not x_48) (not x_57))) +(assert (or (not x_48) (not x_66))) +(assert (or (not x_48) (not x_75))) +(assert (or (not x_48) (not x_84))) +(assert (or (not x_57) (not x_66))) +(assert (or (not x_57) (not x_75))) +(assert (or (not x_57) (not x_84))) +(assert (or (not x_66) (not x_75))) +(assert (or (not x_66) (not x_84))) +(assert (or (not x_75) (not x_84))) +(assert (or (not x_4) (not x_13))) +(assert (or (not x_4) (not x_22))) +(assert (or (not x_4) (not x_31))) +(assert (or (not x_4) (not x_40))) +(assert (or (not x_4) (not x_49))) +(assert (or (not x_4) (not x_58))) +(assert (or (not x_4) (not x_67))) +(assert (or (not x_4) (not x_76))) +(assert (or (not x_4) (not x_85))) +(assert (or (not x_13) (not x_22))) +(assert (or (not x_13) (not x_31))) +(assert (or (not x_13) (not x_40))) +(assert (or (not x_13) (not x_49))) +(assert (or (not x_13) (not x_58))) +(assert (or (not x_13) (not x_67))) +(assert (or (not x_13) (not x_76))) +(assert (or (not x_13) (not x_85))) +(assert (or (not x_22) (not x_31))) +(assert (or (not x_22) (not x_40))) +(assert (or (not x_22) (not x_49))) +(assert (or (not x_22) (not x_58))) +(assert (or (not x_22) (not x_67))) +(assert (or (not x_22) (not x_76))) +(assert (or (not x_22) (not x_85))) +(assert (or (not x_31) (not x_40))) +(assert (or (not x_31) (not x_49))) +(assert (or (not x_31) (not x_58))) +(assert (or (not x_31) (not x_67))) +(assert (or (not x_31) (not x_76))) +(assert (or (not x_31) (not x_85))) +(assert (or (not x_40) (not x_49))) +(assert (or (not x_40) (not x_58))) +(assert (or (not x_40) (not x_67))) +(assert (or (not x_40) (not x_76))) +(assert (or (not x_40) (not x_85))) +(assert (or (not x_49) (not x_58))) +(assert (or (not x_49) (not x_67))) +(assert (or (not x_49) (not x_76))) +(assert (or (not x_49) (not x_85))) +(assert (or (not x_58) (not x_67))) +(assert (or (not x_58) (not x_76))) +(assert (or (not x_58) (not x_85))) +(assert (or (not x_67) (not x_76))) +(assert (or (not x_67) (not x_85))) +(assert (or (not x_76) (not x_85))) +(assert (or (not x_5) (not x_14))) +(assert (or (not x_5) (not x_23))) +(assert (or (not x_5) (not x_32))) +(assert (or (not x_5) (not x_41))) +(assert (or (not x_5) (not x_50))) +(assert (or (not x_5) (not x_59))) +(assert (or (not x_5) (not x_68))) +(assert (or (not x_5) (not x_77))) +(assert (or (not x_5) (not x_86))) +(assert (or (not x_14) (not x_23))) +(assert (or (not x_14) (not x_32))) +(assert (or (not x_14) (not x_41))) +(assert (or (not x_14) (not x_50))) +(assert (or (not x_14) (not x_59))) +(assert (or (not x_14) (not x_68))) +(assert (or (not x_14) (not x_77))) +(assert (or (not x_14) (not x_86))) +(assert (or (not x_23) (not x_32))) +(assert (or (not x_23) (not x_41))) +(assert (or (not x_23) (not x_50))) +(assert (or (not x_23) (not x_59))) +(assert (or (not x_23) (not x_68))) +(assert (or (not x_23) (not x_77))) +(assert (or (not x_23) (not x_86))) +(assert (or (not x_32) (not x_41))) +(assert (or (not x_32) (not x_50))) +(assert (or (not x_32) (not x_59))) +(assert (or (not x_32) (not x_68))) +(assert (or (not x_32) (not x_77))) +(assert (or (not x_32) (not x_86))) +(assert (or (not x_41) (not x_50))) +(assert (or (not x_41) (not x_59))) +(assert (or (not x_41) (not x_68))) +(assert (or (not x_41) (not x_77))) +(assert (or (not x_41) (not x_86))) +(assert (or (not x_50) (not x_59))) +(assert (or (not x_50) (not x_68))) +(assert (or (not x_50) (not x_77))) +(assert (or (not x_50) (not x_86))) +(assert (or (not x_59) (not x_68))) +(assert (or (not x_59) (not x_77))) +(assert (or (not x_59) (not x_86))) +(assert (or (not x_68) (not x_77))) +(assert (or (not x_68) (not x_86))) +(assert (or (not x_77) (not x_86))) +(assert (or (not x_6) (not x_15))) +(assert (or (not x_6) (not x_24))) +(assert (or (not x_6) (not x_33))) +(assert (or (not x_6) (not x_42))) +(assert (or (not x_6) (not x_51))) +(assert (or (not x_6) (not x_60))) +(assert (or (not x_6) (not x_69))) +(assert (or (not x_6) (not x_78))) +(assert (or (not x_6) (not x_87))) +(assert (or (not x_15) (not x_24))) +(assert (or (not x_15) (not x_33))) +(assert (or (not x_15) (not x_42))) +(assert (or (not x_15) (not x_51))) +(assert (or (not x_15) (not x_60))) +(assert (or (not x_15) (not x_69))) +(assert (or (not x_15) (not x_78))) +(assert (or (not x_15) (not x_87))) +(assert (or (not x_24) (not x_33))) +(assert (or (not x_24) (not x_42))) +(assert (or (not x_24) (not x_51))) +(assert (or (not x_24) (not x_60))) +(assert (or (not x_24) (not x_69))) +(assert (or (not x_24) (not x_78))) +(assert (or (not x_24) (not x_87))) +(assert (or (not x_33) (not x_42))) +(assert (or (not x_33) (not x_51))) +(assert (or (not x_33) (not x_60))) +(assert (or (not x_33) (not x_69))) +(assert (or (not x_33) (not x_78))) +(assert (or (not x_33) (not x_87))) +(assert (or (not x_42) (not x_51))) +(assert (or (not x_42) (not x_60))) +(assert (or (not x_42) (not x_69))) +(assert (or (not x_42) (not x_78))) +(assert (or (not x_42) (not x_87))) +(assert (or (not x_51) (not x_60))) +(assert (or (not x_51) (not x_69))) +(assert (or (not x_51) (not x_78))) +(assert (or (not x_51) (not x_87))) +(assert (or (not x_60) (not x_69))) +(assert (or (not x_60) (not x_78))) +(assert (or (not x_60) (not x_87))) +(assert (or (not x_69) (not x_78))) +(assert (or (not x_69) (not x_87))) +(assert (or (not x_78) (not x_87))) +(assert (or (not x_7) (not x_16))) +(assert (or (not x_7) (not x_25))) +(assert (or (not x_7) (not x_34))) +(assert (or (not x_7) (not x_43))) +(assert (or (not x_7) (not x_52))) +(assert (or (not x_7) (not x_61))) +(assert (or (not x_7) (not x_70))) +(assert (or (not x_7) (not x_79))) +(assert (or (not x_7) (not x_88))) +(assert (or (not x_16) (not x_25))) +(assert (or (not x_16) (not x_34))) +(assert (or (not x_16) (not x_43))) +(assert (or (not x_16) (not x_52))) +(assert (or (not x_16) (not x_61))) +(assert (or (not x_16) (not x_70))) +(assert (or (not x_16) (not x_79))) +(assert (or (not x_16) (not x_88))) +(assert (or (not x_25) (not x_34))) +(assert (or (not x_25) (not x_43))) +(assert (or (not x_25) (not x_52))) +(assert (or (not x_25) (not x_61))) +(assert (or (not x_25) (not x_70))) +(assert (or (not x_25) (not x_79))) +(assert (or (not x_25) (not x_88))) +(assert (or (not x_34) (not x_43))) +(assert (or (not x_34) (not x_52))) +(assert (or (not x_34) (not x_61))) +(assert (or (not x_34) (not x_70))) +(assert (or (not x_34) (not x_79))) +(assert (or (not x_34) (not x_88))) +(assert (or (not x_43) (not x_52))) +(assert (or (not x_43) (not x_61))) +(assert (or (not x_43) (not x_70))) +(assert (or (not x_43) (not x_79))) +(assert (or (not x_43) (not x_88))) +(assert (or (not x_52) (not x_61))) +(assert (or (not x_52) (not x_70))) +(assert (or (not x_52) (not x_79))) +(assert (or (not x_52) (not x_88))) +(assert (or (not x_61) (not x_70))) +(assert (or (not x_61) (not x_79))) +(assert (or (not x_61) (not x_88))) +(assert (or (not x_70) (not x_79))) +(assert (or (not x_70) (not x_88))) +(assert (or (not x_79) (not x_88))) +(assert (or (not x_8) (not x_17))) +(assert (or (not x_8) (not x_26))) +(assert (or (not x_8) (not x_35))) +(assert (or (not x_8) (not x_44))) +(assert (or (not x_8) (not x_53))) +(assert (or (not x_8) (not x_62))) +(assert (or (not x_8) (not x_71))) +(assert (or (not x_8) (not x_80))) +(assert (or (not x_8) (not x_89))) +(assert (or (not x_17) (not x_26))) +(assert (or (not x_17) (not x_35))) +(assert (or (not x_17) (not x_44))) +(assert (or (not x_17) (not x_53))) +(assert (or (not x_17) (not x_62))) +(assert (or (not x_17) (not x_71))) +(assert (or (not x_17) (not x_80))) +(assert (or (not x_17) (not x_89))) +(assert (or (not x_26) (not x_35))) +(assert (or (not x_26) (not x_44))) +(assert (or (not x_26) (not x_53))) +(assert (or (not x_26) (not x_62))) +(assert (or (not x_26) (not x_71))) +(assert (or (not x_26) (not x_80))) +(assert (or (not x_26) (not x_89))) +(assert (or (not x_35) (not x_44))) +(assert (or (not x_35) (not x_53))) +(assert (or (not x_35) (not x_62))) +(assert (or (not x_35) (not x_71))) +(assert (or (not x_35) (not x_80))) +(assert (or (not x_35) (not x_89))) +(assert (or (not x_44) (not x_53))) +(assert (or (not x_44) (not x_62))) +(assert (or (not x_44) (not x_71))) +(assert (or (not x_44) (not x_80))) +(assert (or (not x_44) (not x_89))) +(assert (or (not x_53) (not x_62))) +(assert (or (not x_53) (not x_71))) +(assert (or (not x_53) (not x_80))) +(assert (or (not x_53) (not x_89))) +(assert (or (not x_62) (not x_71))) +(assert (or (not x_62) (not x_80))) +(assert (or (not x_62) (not x_89))) +(assert (or (not x_71) (not x_80))) +(assert (or (not x_71) (not x_89))) +(assert (or (not x_80) (not x_89))) +(assert (or (not x_9) (not x_18))) +(assert (or (not x_9) (not x_27))) +(assert (or (not x_9) (not x_36))) +(assert (or (not x_9) (not x_45))) +(assert (or (not x_9) (not x_54))) +(assert (or (not x_9) (not x_63))) +(assert (or (not x_9) (not x_72))) +(assert (or (not x_9) (not x_81))) +(assert (or (not x_9) (not x_90))) +(assert (or (not x_18) (not x_27))) +(assert (or (not x_18) (not x_36))) +(assert (or (not x_18) (not x_45))) +(assert (or (not x_18) (not x_54))) +(assert (or (not x_18) (not x_63))) +(assert (or (not x_18) (not x_72))) +(assert (or (not x_18) (not x_81))) +(assert (or (not x_18) (not x_90))) +(assert (or (not x_27) (not x_36))) +(assert (or (not x_27) (not x_45))) +(assert (or (not x_27) (not x_54))) +(assert (or (not x_27) (not x_63))) +(assert (or (not x_27) (not x_72))) +(assert (or (not x_27) (not x_81))) +(assert (or (not x_27) (not x_90))) +(assert (or (not x_36) (not x_45))) +(assert (or (not x_36) (not x_54))) +(assert (or (not x_36) (not x_63))) +(assert (or (not x_36) (not x_72))) +(assert (or (not x_36) (not x_81))) +(assert (or (not x_36) (not x_90))) +(assert (or (not x_45) (not x_54))) +(assert (or (not x_45) (not x_63))) +(assert (or (not x_45) (not x_72))) +(assert (or (not x_45) (not x_81))) +(assert (or (not x_45) (not x_90))) +(assert (or (not x_54) (not x_63))) +(assert (or (not x_54) (not x_72))) +(assert (or (not x_54) (not x_81))) +(assert (or (not x_54) (not x_90))) +(assert (or (not x_63) (not x_72))) +(assert (or (not x_63) (not x_81))) +(assert (or (not x_63) (not x_90))) +(assert (or (not x_72) (not x_81))) +(assert (or (not x_72) (not x_90))) +(assert (or (not x_81) (not x_90))) +(assert (or (or (or (or (or (or (or (or x_9 x_8) x_7) x_6) x_5) x_4) x_3) x_2) x_1)) +(assert (or (or (or (or (or (or (or (or x_18 x_17) x_16) x_15) x_14) x_13) x_12) x_11) x_10)) +(assert (or (or (or (or (or (or (or (or x_27 x_26) x_25) x_24) x_23) x_22) x_21) x_20) x_19)) +(assert (or (or (or (or (or (or (or (or x_36 x_35) x_34) x_33) x_32) x_31) x_30) x_29) x_28)) +(assert (or (or (or (or (or (or (or (or x_45 x_44) x_43) x_42) x_41) x_40) x_39) x_38) x_37)) +(assert (or (or (or (or (or (or (or (or x_54 x_53) x_52) x_51) x_50) x_49) x_48) x_47) x_46)) +(assert (or (or (or (or (or (or (or (or x_63 x_62) x_61) x_60) x_59) x_58) x_57) x_56) x_55)) +(assert (or (or (or (or (or (or (or (or x_72 x_71) x_70) x_69) x_68) x_67) x_66) x_65) x_64)) +(assert (or (or (or (or (or (or (or (or x_81 x_80) x_79) x_78) x_77) x_76) x_75) x_74) x_73)) +(assert (or (or (or (or (or (or (or (or x_90 x_89) x_88) x_87) x_86) x_85) x_84) x_83) x_82)) +(check-sat) |