mirror of
https://github.com/c-cube/sidekick.git
synced 2026-05-06 01:14:48 -04:00
51 lines
9.5 KiB
Text
51 lines
9.5 KiB
Text
(set-info :smt-lib-version 2.6)
|
|
(set-logic QF_LIA)
|
|
(set-info :source |
|
|
Alberto Griggio
|
|
|
|
|)
|
|
(set-info :category "random")
|
|
(set-info :status sat)
|
|
(declare-fun x0 () Int)
|
|
(declare-fun x1 () Int)
|
|
(declare-fun x2 () Int)
|
|
(declare-fun x3 () Int)
|
|
(declare-fun x4 () Int)
|
|
(declare-fun x5 () Int)
|
|
(declare-fun x6 () Int)
|
|
(declare-fun x7 () Int)
|
|
(declare-fun x8 () Int)
|
|
(declare-fun x9 () Int)
|
|
(declare-fun x10 () Int)
|
|
(declare-fun x11 () Int)
|
|
(declare-fun x12 () Int)
|
|
(declare-fun x13 () Int)
|
|
(declare-fun x14 () Int)
|
|
(declare-fun x15 () Int)
|
|
(declare-fun x16 () Int)
|
|
(declare-fun x17 () Int)
|
|
(declare-fun x18 () Int)
|
|
(declare-fun x19 () Int)
|
|
(declare-fun x20 () Int)
|
|
(declare-fun x21 () Int)
|
|
(declare-fun x22 () Int)
|
|
(declare-fun x23 () Int)
|
|
(declare-fun x24 () Int)
|
|
(declare-fun x25 () Int)
|
|
(declare-fun x26 () Int)
|
|
(declare-fun x27 () Int)
|
|
(declare-fun x28 () Int)
|
|
(declare-fun x29 () Int)
|
|
(declare-fun x30 () Int)
|
|
(declare-fun x31 () Int)
|
|
(declare-fun x32 () Int)
|
|
(declare-fun x33 () Int)
|
|
(declare-fun x34 () Int)
|
|
(declare-fun x35 () Int)
|
|
(declare-fun x36 () Int)
|
|
(declare-fun x37 () Int)
|
|
(declare-fun x38 () Int)
|
|
(declare-fun x39 () Int)
|
|
(assert (let ((?v_51 (* 0 x32)) (?v_0 (* 0 x33)) (?v_12 (* 1 x15)) (?v_19 (* 0 x8)) (?v_71 (* 1 x18)) (?v_3 (* 0 x39)) (?v_27 (* 1 x19)) (?v_42 (* 1 x9)) (?v_35 (* 1 x25)) (?v_55 (* 0 x6)) (?v_4 (* 0 x34)) (?v_54 (* 0 x11)) (?v_61 (* 1 x23)) (?v_104 (* 1 x0)) (?v_29 (* 0 x10)) (?v_25 (* 1 x2)) (?v_13 (* 0 x38)) (?v_5 (* 0 x12)) (?v_1 (* 0 x7)) (?v_18 (* 0 x13)) (?v_20 (* 0 x27)) (?v_14 (* 1 x20)) (?v_10 (* 0 x29)) (?v_15 (* 0 x30)) (?v_22 (* 1 x3)) (?v_26 (* 1 x34)) (?v_88 (* 1 x37)) (?v_9 (* 0 x35)) (?v_78 (* 0 x24)) (?v_52 (* 0 x31)) (?v_17 (* 0 x26)) (?v_38 (* 1 x21)) (?v_31 (* 0 x23)) (?v_43 (* 1 x12)) (?v_16 (* 0 x21)) (?v_33 (* 0 x4)) (?v_21 (* 0 x20)) (?v_24 (* 1 x24)) (?v_28 (* 0 x5)) (?v_23 (* 0 x16)) (?v_57 (* 1 x32)) (?v_85 (* 1 x29)) (?v_32 (* 1 x27)) (?v_2 (* 0 x22)) (?v_59 (* 0 x15)) (?v_101 (* 1 x39)) (?v_30 (* 0 x36)) (?v_53 (* 1 x31)) (?v_83 (* 1 x6)) (?v_48 (* 1 x1)) (?v_67 (* 1 x22)) (?v_74 (* 1 x11)) (?v_82 (* 1 x28)) (?v_47 (* 0 x2)) (?v_99 (* 1 x4)) (?v_75 (* 1 x14)) (?v_56 (* 0 x18)) (?v_94 (* 1 x16)) (?v_86 (* 1 x7)) (?v_65 (* 0 x1)) (?v_72 (* 0 x17)) (?v_69 (* 0 x9)) (?v_73 (* 1 x10)) (?v_81 (* 1 x13)) (?v_91 (* 1 x38)) (?v_70 (* 0 x19)) (?v_106 (* 1 x17)) (?v_110 (* 1 x35)) (?v_8 (* 0 x3)) (?v_103 (* 1 x26)) (?v_98 (* 1 x33)) (?v_90 (* 0 x0)) (?v_112 (* 1 x5)) (?v_68 (* 0 x37)) (?v_95 (* 0 x28)) (?v_97 (* 1 x30)) (?v_102 (* 0 x14)) (?v_107 (* 1 x8)) (?v_100 (* 0 x25)) (?v_114 (* 1 x36)) (?v_116 (* (- 1) x0)) (?v_64 (* (- 1) x5)) (?v_66 (* (- 1) x1)) (?v_6 (* (- 1) x2)) (?v_11 (* (- 1) x11)) (?v_60 (* (- 1) x23)) (?v_37 (* (- 1) x39)) (?v_62 (* (- 1) x38)) (?v_7 (* (- 1) x30)) (?v_77 (* (- 1) x34)) (?v_41 (* (- 1) x28)) (?v_40 (* (- 1) x13)) (?v_39 (* (- 1) x24)) (?v_58 (* (- 1) x22)) (?v_49 (* (- 1) x25)) (?v_44 (* (- 1) x16)) (?v_93 (* (- 1) x35)) (?v_80 (* (- 1) x18)) (?v_36 (* (- 1) x37)) (?v_46 (* (- 1) x32)) (?v_87 (* (- 1) x9)) (?v_34 (* (- 1) x7)) (?v_76 (* (- 1) x6)) (?v_50 (* (- 1) x36)) (?v_89 (* (- 1) x15)) (?v_45 (* (- 1) x14)) (?v_92 (* (- 1) x8)) (?v_63 (* (- 1) x20)) (?v_105 (* (- 1) x17)) (?v_79 (* (- 1) x27)) (?v_111 (* (- 1) x31)) (?v_84 (* (- 1) x3)) (?v_96 (* (- 1) x4)) (?v_115 (* (- 1) x26)) (?v_108 (* (- 1) x29)) (?v_109 (* (- 1) x19)) (?v_113 (* (- 1) x10))) (and (<= (+ ?v_51 ?v_17 ?v_116 ?v_0 ?v_8 ?v_30 ?v_12 ?v_19 ?v_71 ?v_3 ?v_9 ?v_2 ?v_64 ?v_27 ?v_1 ?v_66 ?v_6 ?v_11 ?v_60 ?v_42 ?v_35 ?v_55 ?v_16 ?v_0 ?v_37 ?v_62 ?v_4 ?v_21 ?v_54 ?v_7 ?v_1 ?v_61 ?v_104 ?v_77 ?v_2 ?v_3 ?v_4 ?v_10 ?v_29 ?v_25) (- 1)) (<= (+ ?v_13 ?v_5 ?v_5 ?v_6 ?v_41 ?v_40 ?v_7 ?v_8 ?v_9 ?v_1 ?v_39 ?v_18 ?v_20 ?v_14 ?v_58 ?v_49 ?v_10 ?v_23 ?v_11 ?v_15 ?v_12 ?v_13 ?v_22 ?v_26 ?v_44 ?v_88 ?v_9 ?v_3 ?v_95 ?v_14 ?v_93 ?v_78 ?v_52 ?v_15 ?v_16 ?v_17 ?v_80 ?v_4 ?v_38 ?v_31) 0) (<= (+ ?v_43 ?v_36 ?v_18 ?v_19 ?v_16 ?v_33 ?v_20 ?v_56 ?v_21 ?v_24 ?v_28 ?v_46 ?v_18 ?v_2 ?v_9 ?v_87 ?v_22 ?v_23 ?v_13 ?v_34 ?v_24 ?v_3 ?v_10 ?v_57 ?v_14 ?v_18 ?v_85 ?v_18 ?v_32 ?v_76 ?v_2 ?v_3 ?v_59 ?v_25 ?v_26 ?v_5 ?v_27 ?v_17 ?v_14 ?v_28) 1) (<= (+ ?v_22 ?v_50 ?v_1 ?v_29 ?v_101 ?v_12 ?v_2 ?v_30 ?v_89 ?v_31 ?v_70 ?v_32 ?v_33 ?v_34 ?v_24 ?v_18 ?v_29 ?v_21 ?v_53 ?v_0 ?v_35 ?v_16 ?v_83 ?v_18 ?v_36 ?v_47 ?v_37 ?v_45 ?v_38 ?v_39 ?v_68 ?v_92 ?v_40 ?v_41 ?v_13 ?v_26 ?v_42 ?v_19 ?v_30 ?v_43) (- 1)) (<= (+ ?v_27 ?v_34 ?v_48 ?v_44 ?v_45 ?v_67 ?v_30 ?v_8 ?v_20 ?v_40 ?v_32 ?v_29 ?v_46 ?v_4 ?v_40 ?v_74 ?v_11 ?v_82 ?v_47 ?v_36 ?v_99 ?v_2 ?v_48 ?v_49 ?v_5 ?v_50 ?v_27 ?v_69 ?v_65 ?v_51 ?v_2 ?v_52 ?v_29 ?v_34 ?v_52 ?v_23 ?v_23 ?v_30 ?v_53 ?v_20) 0) (<= (+ ?v_54 ?v_55 ?v_102 ?v_75 ?v_9 ?v_56 ?v_18 ?v_57 ?v_13 ?v_63 ?v_58 ?v_4 ?v_0 ?v_5 ?v_59 ?v_52 ?v_15 ?v_60 ?v_48 ?v_15 ?v_54 ?v_94 ?v_34 ?v_60 ?v_61 ?v_86 ?v_31 ?v_28 ?v_62 ?v_37 ?v_63 ?v_17 ?v_52 ?v_57 ?v_8 ?v_38 ?v_2 ?v_64 ?v_65 ?v_66) 0) (<= (+ ?v_72 ?v_6 ?v_55 ?v_0 ?v_14 ?v_30 ?v_105 ?v_4 ?v_37 ?v_51 ?v_67 ?v_54 ?v_33 ?v_17 ?v_29 ?v_68 ?v_69 ?v_8 ?v_70 ?v_67 ?v_71 ?v_0 ?v_73 ?v_81 ?v_45 ?v_72 ?v_40 ?v_31 ?v_39 ?v_65 ?v_79 ?v_57 ?v_73 ?v_45 ?v_7 ?v_91 ?v_17 ?v_40 ?v_31 ?v_69) 1) (<= (+ ?v_56 ?v_74 ?v_66 ?v_75 ?v_76 ?v_43 ?v_22 ?v_28 ?v_28 ?v_11 ?v_19 ?v_58 ?v_1 ?v_77 ?v_74 ?v_64 ?v_70 ?v_62 ?v_33 ?v_24 ?v_5 ?v_72 ?v_72 ?v_17 ?v_4 ?v_111 ?v_54 ?v_33 ?v_65 ?v_33 ?v_3 ?v_16 ?v_106 ?v_5 ?v_5 ?v_78 ?v_14 ?v_79 ?v_80 ?v_60) 1) (<= (+ ?v_0 ?v_81 ?v_59 ?v_69 ?v_31 ?v_36 ?v_34 ?v_110 ?v_40 ?v_55 ?v_29 ?v_0 ?v_82 ?v_83 ?v_65 ?v_84 ?v_23 ?v_96 ?v_29 ?v_21 ?v_8 ?v_29 ?v_63 ?v_8 ?v_68 ?v_103 ?v_52 ?v_15 ?v_84 ?v_85 ?v_86 ?v_54 ?v_62 ?v_98 ?v_33 ?v_13 ?v_18 ?v_44 ?v_65 ?v_67) 0) (<= (+ ?v_48 ?v_9 ?v_83 ?v_4 ?v_78 ?v_4 ?v_78 ?v_90 ?v_73 ?v_41 ?v_72 ?v_17 ?v_38 (* (- 1) x12) ?v_10 ?v_29 ?v_9 ?v_55 ?v_1 ?v_71 ?v_62 ?v_3 ?v_32 ?v_70 ?v_70 ?v_71 ?v_14 ?v_74 ?v_58 ?v_10 ?v_21 ?v_85 ?v_70 ?v_21 ?v_63 ?v_87 ?v_12 ?v_112 ?v_20 ?v_88) 0) (<= (+ ?v_31 ?v_82 ?v_51 ?v_0 ?v_17 ?v_31 ?v_22 ?v_10 ?v_27 ?v_31 ?v_100 ?v_3 ?v_28 ?v_55 ?v_60 ?v_51 ?v_89 ?v_86 ?v_68 ?v_57 ?v_56 ?v_80 ?v_69 ?v_36 ?v_47 ?v_46 ?v_44 ?v_85 ?v_21 ?v_115 ?v_14 ?v_17 ?v_90 ?v_7 ?v_91 ?v_73 ?v_77 ?v_92 ?v_27 ?v_82) (- 1)) (<= (+ ?v_14 ?v_77 ?v_93 ?v_59 ?v_9 ?v_48 ?v_94 ?v_34 ?v_95 ?v_91 ?v_92 ?v_96 ?v_27 ?v_43 ?v_31 ?v_97 ?v_87 ?v_82 ?v_81 ?v_91 ?v_77 ?v_79 ?v_25 ?v_68 ?v_54 ?v_68 ?v_52 ?v_92 ?v_54 ?v_97 ?v_96 ?v_98 ?v_46 ?v_14 ?v_99 ?v_95 ?v_50 ?v_55 ?v_100 ?v_0) 0) (<= (+ ?v_29 ?v_60 ?v_1 ?v_68 ?v_87 ?v_87 ?v_53 ?v_31 ?v_37 ?v_50 ?v_46 ?v_78 ?v_64 ?v_28 ?v_79 ?v_21 ?v_78 ?v_37 ?v_79 ?v_21 ?v_21 ?v_2 ?v_47 ?v_85 ?v_56 ?v_101 ?v_31 ?v_100 ?v_67 ?v_87 ?v_36 ?v_64 ?v_23 ?v_102 ?v_99 ?v_4 ?v_103 ?v_8 ?v_91 ?v_104) 0) (<= (+ ?v_26 ?v_0 ?v_80 ?v_73 ?v_79 ?v_80 ?v_101 ?v_73 ?v_58 ?v_60 ?v_17 ?v_30 ?v_0 ?v_13 ?v_21 ?v_63 ?v_84 ?v_43 ?v_63 ?v_95 ?v_25 ?v_74 ?v_15 ?v_93 ?v_7 ?v_90 ?v_54 ?v_63 ?v_12 ?v_62 ?v_51 ?v_15 ?v_103 ?v_2 ?v_88 ?v_6 ?v_58 ?v_105 ?v_40 ?v_56) 1) (<= (+ ?v_22 ?v_101 ?v_103 ?v_71 ?v_64 ?v_108 ?v_12 ?v_59 ?v_107 ?v_60 ?v_75 ?v_49 ?v_55 ?v_100 ?v_52 ?v_39 ?v_48 ?v_95 ?v_77 ?v_87 ?v_100 ?v_24 ?v_51 ?v_39 ?v_95 ?v_92 ?v_39 ?v_1 ?v_106 ?v_107 ?v_109 ?v_68 ?v_108 ?v_64 ?v_57 ?v_56 ?v_65 ?v_21 ?v_109 ?v_55) (- 1)) (<= (+ ?v_0 ?v_0 ?v_110 ?v_83 ?v_93 ?v_66 ?v_65 ?v_69 ?v_17 ?v_102 ?v_7 ?v_21 ?v_89 ?v_52 ?v_25 ?v_2 ?v_85 ?v_2 ?v_106 ?v_12 ?v_110 ?v_21 ?v_13 ?v_89 ?v_1 ?v_90 ?v_27 ?v_30 ?v_90 ?v_79 ?v_56 ?v_21 ?v_33 ?v_16 ?v_63 ?v_13 ?v_4 ?v_93 ?v_103 ?v_107) 1) (<= (+ ?v_27 ?v_73 ?v_72 ?v_67 ?v_79 ?v_44 ?v_69 ?v_14 ?v_110 (* (- 1) x21) ?v_99 ?v_13 ?v_3 ?v_44 ?v_75 ?v_79 ?v_46 ?v_70 ?v_95 ?v_28 ?v_113 ?v_83 ?v_91 ?v_89 ?v_85 ?v_101 ?v_52 ?v_98 ?v_55 ?v_102 ?v_2 ?v_1 ?v_16 ?v_72 ?v_39 ?v_2 ?v_54 ?v_107 ?v_100 ?v_54) 1) (<= (+ ?v_98 ?v_72 ?v_1 ?v_85 ?v_92 ?v_22 ?v_90 ?v_100 ?v_71 ?v_4 ?v_72 ?v_61 ?v_19 ?v_18 ?v_25 ?v_111 ?v_70 ?v_78 ?v_43 ?v_30 ?v_51 ?v_83 ?v_33 ?v_74 ?v_54 ?v_29 ?v_32 ?v_2 ?v_63 ?v_35 ?v_67 ?v_85 ?v_97 ?v_106 ?v_20 ?v_41 ?v_37 ?v_68 ?v_52 ?v_91) 0) (<= (+ ?v_101 ?v_78 ?v_54 ?v_109 ?v_30 ?v_54 ?v_112 ?v_77 ?v_2 ?v_55 ?v_72 ?v_112 ?v_52 ?v_25 ?v_23 ?v_20 ?v_59 ?v_25 ?v_1 ?v_65 ?v_13 ?v_22 ?v_67 ?v_90 ?v_33 ?v_55 ?v_55 ?v_57 ?v_64 ?v_6 ?v_18 ?v_75 ?v_16 ?v_36 ?v_77 ?v_59 ?v_78 ?v_56 ?v_35 ?v_4) 0) (<= (+ ?v_67 ?v_78 ?v_35 ?v_113 ?v_93 ?v_0 ?v_17 ?v_19 ?v_41 ?v_58 ?v_64 ?v_114 ?v_20 ?v_106 ?v_93 ?v_3 ?v_114 ?v_73 ?v_102 ?v_4 ?v_33 ?v_106 ?v_107 ?v_55 ?v_64 ?v_5 ?v_54 ?v_68 ?v_113 ?v_50 ?v_19 ?v_9 ?v_67 ?v_17 ?v_69 ?v_55 ?v_8 ?v_17 ?v_6 ?v_35) (- 1)) (<= (+ ?v_86 ?v_51 ?v_100 ?v_95 ?v_50 ?v_3 ?v_110 ?v_26 ?v_9 ?v_53 ?v_95 ?v_80 ?v_113 ?v_71 ?v_35 ?v_73 ?v_35 ?v_54 ?v_115 ?v_17 ?v_99 ?v_22 ?v_114 ?v_87 ?v_33 ?v_32 ?v_77 ?v_47 ?v_45 ?v_101 ?v_107 ?v_65 ?v_113 ?v_22 ?v_56 ?v_22 ?v_30 ?v_17 ?v_59 ?v_2) (- 1)) (<= (+ ?v_18 ?v_77 ?v_98 ?v_63 ?v_43 ?v_20 ?v_77 ?v_99 ?v_22 ?v_80 ?v_30 ?v_67 ?v_47 ?v_79 ?v_18 ?v_95 ?v_100 ?v_55 ?v_113 ?v_30 ?v_70 ?v_103 ?v_93 ?v_116 ?v_40 ?v_68 ?v_70 ?v_79 ?v_30 ?v_16 ?v_5 ?v_2 ?v_1 ?v_53 ?v_8 ?v_53 ?v_51 ?v_31 ?v_87 ?v_100) 1) (<= (+ ?v_24 ?v_106 ?v_78 ?v_12 ?v_28 ?v_15 ?v_56 ?v_24 ?v_29 ?v_36 ?v_21 ?v_56 ?v_100 ?v_17 ?v_77 ?v_37 ?v_63 ?v_36 ?v_112 ?v_32 ?v_106 ?v_53 ?v_114 ?v_2 ?v_78 ?v_32 ?v_18 ?v_101 ?v_51 ?v_22 ?v_47 ?v_2 ?v_61 ?v_111 ?v_14 ?v_95 ?v_64 ?v_65 ?v_116 ?v_33) (- 1)) (<= (+ ?v_8 ?v_9 ?v_83 ?v_102 ?v_5 ?v_0 ?v_106 ?v_65 ?v_31 ?v_85 ?v_85 ?v_102 ?v_38 ?v_23 ?v_15 ?v_30 ?v_55 ?v_74 ?v_36 ?v_55 ?v_98 ?v_21 ?v_2 ?v_31 ?v_9 ?v_28 ?v_47 ?v_95 ?v_20 ?v_71 ?v_53 ?v_8 ?v_8 ?v_16 ?v_3 ?v_45 ?v_56 ?v_2 ?v_93 ?v_23) 0) (<= (+ ?v_91 ?v_93 ?v_16 ?v_13 ?v_79 ?v_57 ?v_5 ?v_56 ?v_52 ?v_72 ?v_48 ?v_74 ?v_102 ?v_90 ?v_13 ?v_84 ?v_27 ?v_4 ?v_70 ?v_0 ?v_115 ?v_26 ?v_5 ?v_31 ?v_35 ?v_94 ?v_51 ?v_15 ?v_2 ?v_90 ?v_39 ?v_84 ?v_14 ?v_25 ?v_100 ?v_97 ?v_19 ?v_21 ?v_95 ?v_100) 0))))
|
|
(check-sat)
|
|
(exit)
|