diff options
Diffstat (limited to 'test/regress/regress2/arith/sc-7.base.cvc.smt')
| -rw-r--r-- | test/regress/regress2/arith/sc-7.base.cvc.smt | 164 |
1 files changed, 164 insertions, 0 deletions
diff --git a/test/regress/regress2/arith/sc-7.base.cvc.smt b/test/regress/regress2/arith/sc-7.base.cvc.smt new file mode 100644 index 000000000..72a561593 --- /dev/null +++ b/test/regress/regress2/arith/sc-7.base.cvc.smt @@ -0,0 +1,164 @@ +(benchmark synch_circuit + :source { +Fully parameterized specification and verification of a synchronizer +circuit modeling metastability at various levels of refinement. +A paper describing this specification, to be published in Designing +Correct Circuits (DCC), 2006, is available from the authors. + +Geoffrey Brown, Indiana University <geobrown@cs.indiana.edu> +Lee Pike, Galois Connections, Inc. <leepike@galois.com> + +Translated into CVC format by Leonardo de Moura. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite + +} + :status unsat +:category { industrial } +:difficulty { 0 } + :logic QF_LRA + + :extrapreds ((x_0)) + :extrapreds ((x_1)) + :extrafuns ((x_2 Real)) + :extrapreds ((x_3)) + :extrapreds ((x_4)) + :extrapreds ((x_5)) + :extrafuns ((x_6 Real)) + :extrapreds ((x_7)) + :extrafuns ((x_8 Real)) + :extrafuns ((x_9 Real)) + :extrafuns ((x_10 Real)) + :extrafuns ((x_11 Real)) + :extrafuns ((x_12 Real)) + :extrapreds ((x_13)) + :extrafuns ((x_14 Real)) + :extrafuns ((x_15 Real)) + :extrafuns ((x_16 Real)) + :extrafuns ((x_17 Real)) + :extrafuns ((x_18 Real)) + :extrafuns ((x_19 Real)) + :extrapreds ((x_20)) + :extrapreds ((x_21)) + :extrapreds ((x_22)) + :extrapreds ((x_23)) + :extrafuns ((x_24 Real)) + :extrapreds ((x_25)) + :extrafuns ((x_26 Real)) + :extrafuns ((x_27 Real)) + :extrafuns ((x_28 Real)) + :extrafuns ((x_29 Real)) + :extrafuns ((x_30 Real)) + :extrafuns ((x_31 Real)) + :extrafuns ((x_32 Real)) + :extrafuns ((x_33 Real)) + :extrafuns ((x_34 Real)) + :extrafuns ((x_35 Real)) + :extrafuns ((x_36 Real)) + :extrapreds ((x_37)) + :extrafuns ((x_38 Real)) + :extrafuns ((x_39 Real)) + :extrapreds ((x_40)) + :extrapreds ((x_41)) + :extrapreds ((x_42)) + :extrapreds ((x_43)) + :extrafuns ((x_44 Real)) + :extrapreds ((x_45)) + :extrafuns ((x_46 Real)) + :extrafuns ((x_47 Real)) + :extrafuns ((x_48 Real)) + :extrafuns ((x_49 Real)) + :extrafuns ((x_50 Real)) + :extrafuns ((x_51 Real)) + :extrafuns ((x_52 Real)) + :extrafuns ((x_53 Real)) + :extrafuns ((x_54 Real)) + :extrapreds ((x_55)) + :extrafuns ((x_56 Real)) + :extrafuns ((x_57 Real)) + :extrapreds ((x_58)) + :extrapreds ((x_59)) + :extrapreds ((x_60)) + :extrapreds ((x_61)) + :extrafuns ((x_62 Real)) + :extrapreds ((x_63)) + :extrafuns ((x_64 Real)) + :extrafuns ((x_65 Real)) + :extrafuns ((x_66 Real)) + :extrafuns ((x_67 Real)) + :extrafuns ((x_68 Real)) + :extrafuns ((x_69 Real)) + :extrafuns ((x_70 Real)) + :extrafuns ((x_71 Real)) + :extrafuns ((x_72 Real)) + :extrapreds ((x_73)) + :extrafuns ((x_74 Real)) + :extrafuns ((x_75 Real)) + :extrapreds ((x_76)) + :extrapreds ((x_77)) + :extrapreds ((x_78)) + :extrapreds ((x_79)) + :extrafuns ((x_80 Real)) + :extrapreds ((x_81)) + :extrafuns ((x_82 Real)) + :extrafuns ((x_83 Real)) + :extrafuns ((x_84 Real)) + :extrafuns ((x_85 Real)) + :extrafuns ((x_86 Real)) + :extrafuns ((x_87 Real)) + :extrafuns ((x_88 Real)) + :extrafuns ((x_89 Real)) + :extrafuns ((x_90 Real)) + :extrapreds ((x_91)) + :extrafuns ((x_92 Real)) + :extrafuns ((x_93 Real)) + :extrapreds ((x_94)) + :extrapreds ((x_95)) + :extrapreds ((x_96)) + :extrapreds ((x_97)) + :extrafuns ((x_98 Real)) + :extrapreds ((x_99)) + :extrafuns ((x_100 Real)) + :extrafuns ((x_101 Real)) + :extrafuns ((x_102 Real)) + :extrafuns ((x_103 Real)) + :extrafuns ((x_104 Real)) + :extrafuns ((x_105 Real)) + :extrafuns ((x_106 Real)) + :extrafuns ((x_107 Real)) + :extrafuns ((x_108 Real)) + :extrapreds ((x_109)) + :extrafuns ((x_110 Real)) + :extrafuns ((x_111 Real)) + :extrapreds ((x_112)) + :extrapreds ((x_113)) + :extrapreds ((x_114)) + :extrapreds ((x_115)) + :extrafuns ((x_116 Real)) + :extrapreds ((x_117)) + :extrafuns ((x_118 Real)) + :extrafuns ((x_119 Real)) + :extrafuns ((x_120 Real)) + :extrafuns ((x_121 Real)) + :extrafuns ((x_122 Real)) + :extrafuns ((x_123 Real)) + :extrafuns ((x_124 Real)) + :extrafuns ((x_125 Real)) + :extrafuns ((x_126 Real)) + :extrapreds ((x_127)) + :extrafuns ((x_128 Real)) + :extrafuns ((x_129 Real)) + :extrapreds ((x_130)) + :extrapreds ((x_131)) + :extrapreds ((x_132)) + :extrapreds ((x_133)) + :extrafuns ((x_134 Real)) + :extrapreds ((x_135)) + :extrafuns ((x_136 Real)) + :extrafuns ((x_137 Real)) + :extrafuns ((x_138 Real)) + :extrafuns ((x_139 Real)) + :formula +(flet ($cvcl_80 (= x_6 x_9)) (flet ($cvcl_77 (= x_2 x_11)) (flet ($cvcl_82 (not $cvcl_77)) (flet ($cvcl_73 (iff x_13 x_7)) (flet ($cvcl_74 (= x_14 x_15)) (let (?cvcl_78 (ite (<= x_6 x_2) x_6 x_2)) (let (?cvcl_72 (ite (<= x_2 x_6) x_2 x_6)) (flet ($cvcl_66 (= x_32 x_8)) (flet ($cvcl_67 (= x_9 x_33)) (flet ($cvcl_68 (= x_34 x_10)) (flet ($cvcl_64 (= x_11 x_35)) (flet ($cvcl_69 (not $cvcl_64)) (flet ($cvcl_71 (= x_36 x_12)) (flet ($cvcl_61 (iff x_37 x_13)) (flet ($cvcl_62 (= x_38 x_14)) (let (?cvcl_65 (ite (<= x_9 x_11) x_9 x_11)) (let (?cvcl_60 (ite (<= x_11 x_9) x_11 x_9)) (flet ($cvcl_54 (= x_50 x_32)) (flet ($cvcl_55 (= x_33 x_51)) (flet ($cvcl_56 (= x_52 x_34)) (flet ($cvcl_52 (= x_35 x_53)) (flet ($cvcl_57 (not $cvcl_52)) (flet ($cvcl_59 (= x_54 x_36)) (flet ($cvcl_49 (iff x_55 x_37)) (flet ($cvcl_50 (= x_56 x_38)) (let (?cvcl_53 (ite (<= x_33 x_35) x_33 x_35)) (let (?cvcl_48 (ite (<= x_35 x_33) x_35 x_33)) (flet ($cvcl_42 (= x_68 x_50)) (flet ($cvcl_43 (= x_51 x_69)) (flet ($cvcl_44 (= x_70 x_52)) (flet ($cvcl_40 (= x_53 x_71)) (flet ($cvcl_45 (not $cvcl_40)) (flet ($cvcl_47 (= x_72 x_54)) (flet ($cvcl_37 (iff x_73 x_55)) (flet ($cvcl_38 (= x_74 x_56)) (let (?cvcl_41 (ite (<= x_51 x_53) x_51 x_53)) (let (?cvcl_36 (ite (<= x_53 x_51) x_53 x_51)) (flet ($cvcl_30 (= x_86 x_68)) (flet ($cvcl_31 (= x_69 x_87)) (flet ($cvcl_32 (= x_88 x_70)) (flet ($cvcl_28 (= x_71 x_89)) (flet ($cvcl_33 (not $cvcl_28)) (flet ($cvcl_35 (= x_90 x_72)) (flet ($cvcl_25 (iff x_91 x_73)) (flet ($cvcl_26 (= x_92 x_74)) (let (?cvcl_29 (ite (<= x_69 x_71) x_69 x_71)) (let (?cvcl_24 (ite (<= x_71 x_69) x_71 x_69)) (flet ($cvcl_18 (= x_104 x_86)) (flet ($cvcl_19 (= x_87 x_105)) (flet ($cvcl_20 (= x_106 x_88)) (flet ($cvcl_16 (= x_89 x_107)) (flet ($cvcl_21 (not $cvcl_16)) (flet ($cvcl_23 (= x_108 x_90)) (flet ($cvcl_13 (iff x_109 x_91)) (flet ($cvcl_14 (= x_110 x_92)) (let (?cvcl_17 (ite (<= x_87 x_89) x_87 x_89)) (let (?cvcl_12 (ite (<= x_89 x_87) x_89 x_87)) (flet ($cvcl_6 (= x_122 x_104)) (flet ($cvcl_7 (= x_105 x_123)) (flet ($cvcl_8 (= x_124 x_106)) (flet ($cvcl_4 (= x_107 x_125)) (flet ($cvcl_9 (not $cvcl_4)) (flet ($cvcl_11 (= x_126 x_108)) (flet ($cvcl_1 (iff x_127 x_109)) (flet ($cvcl_2 (= x_128 x_110)) (let (?cvcl_5 (ite (<= x_105 x_107) x_105 x_107)) (let (?cvcl_0 (ite (<= x_107 x_105) x_107 x_105)) (flet ($cvcl_75 (not x_7)) (flet ($cvcl_3 (iff x_131 x_113)) (flet ($cvcl_10 (= x_110 x_128)) (flet ($cvcl_15 (iff x_113 x_95)) (flet ($cvcl_22 (= x_92 x_110)) (flet ($cvcl_27 (iff x_95 x_77)) (flet ($cvcl_34 (= x_74 x_92)) (flet ($cvcl_39 (iff x_77 x_59)) (flet ($cvcl_46 (= x_56 x_74)) (flet ($cvcl_51 (iff x_59 x_41)) (flet ($cvcl_58 (= x_38 x_56)) (flet ($cvcl_63 (iff x_41 x_21)) (flet ($cvcl_70 (= x_14 x_38)) (flet ($cvcl_76 (iff x_21 x_3)) (flet ($cvcl_84 (= x_15 x_14)) (flet ($cvcl_83 (not (>= ?cvcl_78 0))) (flet ($cvcl_79 (= x_8 0)) (flet ($cvcl_81 (= x_10 0)) (flet ($cvcl_85 (= x_12 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (> x_16 0) (> x_17 0)) (>= x_18 0)) (< x_18 x_16)) (< x_18 x_17)) (>= x_30 0)) (< x_30 x_16)) (< x_30 x_17)) (not x_0)) (not x_1)) (>= x_2 0)) (not x_3)) (not x_4)) (not x_5)) (>= x_6 0)) $cvcl_75) (or (and (and (and (and (and (and (and (and (and (= x_129 0) (iff x_130 x_117)) (= ?cvcl_0 x_107)) (<= (+ ?cvcl_0 x_16) x_125)) (or $cvcl_3 (iff x_131 x_112) )) (iff x_132 x_114)) (iff x_133 x_115)) (= x_123 x_105)) $cvcl_1) $cvcl_2) (and (and (and (and (and (and (and (and (and (= x_129 1) (iff x_133 x_114)) (= ?cvcl_0 x_105)) (<= (+ ?cvcl_0 x_17) x_123)) (or (and (and (= x_134 0) $cvcl_1) $cvcl_2) (and (and (= x_134 1) (iff x_109 x_115)) (iff x_127 (not x_109))) )) (iff x_135 x_117)) (iff x_130 x_112)) (= x_136 x_118)) (= x_125 x_107)) $cvcl_3) )) (or (or (and (and (and (= x_137 0) $cvcl_9) (or (not (<= x_104 ?cvcl_5)) (iff x_135 x_109) )) $cvcl_6) (and (and (and (= x_137 1) $cvcl_4) (xor x_109 x_127 )) (= x_122 (+ ?cvcl_5 x_18))) ) (and (and (and (= x_137 2) $cvcl_4) (iff x_109 x_127)) $cvcl_6) )) (or (or (and (and (and (= x_138 0) (not $cvcl_7)) (or (not (<= x_106 ?cvcl_0)) (iff x_132 x_113) )) $cvcl_8) (and (and (and (= x_138 1) $cvcl_7) (xor x_113 x_131 )) (= x_124 (+ ?cvcl_0 x_30))) ) (and (and (and (= x_138 2) $cvcl_7) (iff x_113 x_131)) $cvcl_8) )) (or (or (and (and (and (= x_139 0) $cvcl_9) (or (not (<= x_108 ?cvcl_5)) (= x_136 x_110) )) $cvcl_11) (and (and (and (= x_139 1) $cvcl_4) (not $cvcl_10)) (= x_126 (+ ?cvcl_5 x_18))) ) (and (and (and (= x_139 2) $cvcl_4) $cvcl_10) $cvcl_11) )) (or (and (and (and (and (and (and (and (and (and (= x_111 0) (iff x_112 x_99)) (= ?cvcl_12 x_89)) (<= (+ ?cvcl_12 x_16) x_107)) (or $cvcl_15 (iff x_113 x_94) )) (iff x_114 x_96)) (iff x_115 x_97)) (= x_105 x_87)) $cvcl_13) $cvcl_14) (and (and (and (and (and (and (and (and (and (= x_111 1) (iff x_115 x_96)) (= ?cvcl_12 x_87)) (<= (+ ?cvcl_12 x_17) x_105)) (or (and (and (= x_116 0) $cvcl_13) $cvcl_14) (and (and (= x_116 1) (iff x_91 x_97)) (iff x_109 (not x_91))) )) (iff x_117 x_99)) (iff x_112 x_94)) (= x_118 x_100)) (= x_107 x_89)) $cvcl_15) )) (or (or (and (and (and (= x_119 0) $cvcl_21) (or (not (<= x_86 ?cvcl_17)) (iff x_117 x_91) )) $cvcl_18) (and (and (and (= x_119 1) $cvcl_16) (xor x_91 x_109 )) (= x_104 (+ ?cvcl_17 x_18))) ) (and (and (and (= x_119 2) $cvcl_16) (iff x_91 x_109)) $cvcl_18) )) (or (or (and (and (and (= x_120 0) (not $cvcl_19)) (or (not (<= x_88 ?cvcl_12)) (iff x_114 x_95) )) $cvcl_20) (and (and (and (= x_120 1) $cvcl_19) (xor x_95 x_113 )) (= x_106 (+ ?cvcl_12 x_30))) ) (and (and (and (= x_120 2) $cvcl_19) (iff x_95 x_113)) $cvcl_20) )) (or (or (and (and (and (= x_121 0) $cvcl_21) (or (not (<= x_90 ?cvcl_17)) (= x_118 x_92) )) $cvcl_23) (and (and (and (= x_121 1) $cvcl_16) (not $cvcl_22)) (= x_108 (+ ?cvcl_17 x_18))) ) (and (and (and (= x_121 2) $cvcl_16) $cvcl_22) $cvcl_23) )) (or (and (and (and (and (and (and (and (and (and (= x_93 0) (iff x_94 x_81)) (= ?cvcl_24 x_71)) (<= (+ ?cvcl_24 x_16) x_89)) (or $cvcl_27 (iff x_95 x_76) )) (iff x_96 x_78)) (iff x_97 x_79)) (= x_87 x_69)) $cvcl_25) $cvcl_26) (and (and (and (and (and (and (and (and (and (= x_93 1) (iff x_97 x_78)) (= ?cvcl_24 x_69)) (<= (+ ?cvcl_24 x_17) x_87)) (or (and (and (= x_98 0) $cvcl_25) $cvcl_26) (and (and (= x_98 1) (iff x_73 x_79)) (iff x_91 (not x_73))) )) (iff x_99 x_81)) (iff x_94 x_76)) (= x_100 x_82)) (= x_89 x_71)) $cvcl_27) )) (or (or (and (and (and (= x_101 0) $cvcl_33) (or (not (<= x_68 ?cvcl_29)) (iff x_99 x_73) )) $cvcl_30) (and (and (and (= x_101 1) $cvcl_28) (xor x_73 x_91 )) (= x_86 (+ ?cvcl_29 x_18))) ) (and (and (and (= x_101 2) $cvcl_28) (iff x_73 x_91)) $cvcl_30) )) (or (or (and (and (and (= x_102 0) (not $cvcl_31)) (or (not (<= x_70 ?cvcl_24)) (iff x_96 x_77) )) $cvcl_32) (and (and (and (= x_102 1) $cvcl_31) (xor x_77 x_95 )) (= x_88 (+ ?cvcl_24 x_30))) ) (and (and (and (= x_102 2) $cvcl_31) (iff x_77 x_95)) $cvcl_32) )) (or (or (and (and (and (= x_103 0) $cvcl_33) (or (not (<= x_72 ?cvcl_29)) (= x_100 x_74) )) $cvcl_35) (and (and (and (= x_103 1) $cvcl_28) (not $cvcl_34)) (= x_90 (+ ?cvcl_29 x_18))) ) (and (and (and (= x_103 2) $cvcl_28) $cvcl_34) $cvcl_35) )) (or (and (and (and (and (and (and (and (and (and (= x_75 0) (iff x_76 x_63)) (= ?cvcl_36 x_53)) (<= (+ ?cvcl_36 x_16) x_71)) (or $cvcl_39 (iff x_77 x_58) )) (iff x_78 x_60)) (iff x_79 x_61)) (= x_69 x_51)) $cvcl_37) $cvcl_38) (and (and (and (and (and (and (and (and (and (= x_75 1) (iff x_79 x_60)) (= ?cvcl_36 x_51)) (<= (+ ?cvcl_36 x_17) x_69)) (or (and (and (= x_80 0) $cvcl_37) $cvcl_38) (and (and (= x_80 1) (iff x_55 x_61)) (iff x_73 (not x_55))) )) (iff x_81 x_63)) (iff x_76 x_58)) (= x_82 x_64)) (= x_71 x_53)) $cvcl_39) )) (or (or (and (and (and (= x_83 0) $cvcl_45) (or (not (<= x_50 ?cvcl_41)) (iff x_81 x_55) )) $cvcl_42) (and (and (and (= x_83 1) $cvcl_40) (xor x_55 x_73 )) (= x_68 (+ ?cvcl_41 x_18))) ) (and (and (and (= x_83 2) $cvcl_40) (iff x_55 x_73)) $cvcl_42) )) (or (or (and (and (and (= x_84 0) (not $cvcl_43)) (or (not (<= x_52 ?cvcl_36)) (iff x_78 x_59) )) $cvcl_44) (and (and (and (= x_84 1) $cvcl_43) (xor x_59 x_77 )) (= x_70 (+ ?cvcl_36 x_30))) ) (and (and (and (= x_84 2) $cvcl_43) (iff x_59 x_77)) $cvcl_44) )) (or (or (and (and (and (= x_85 0) $cvcl_45) (or (not (<= x_54 ?cvcl_41)) (= x_82 x_56) )) $cvcl_47) (and (and (and (= x_85 1) $cvcl_40) (not $cvcl_46)) (= x_72 (+ ?cvcl_41 x_18))) ) (and (and (and (= x_85 2) $cvcl_40) $cvcl_46) $cvcl_47) )) (or (and (and (and (and (and (and (and (and (and (= x_57 0) (iff x_58 x_45)) (= ?cvcl_48 x_35)) (<= (+ ?cvcl_48 x_16) x_53)) (or $cvcl_51 (iff x_59 x_40) )) (iff x_60 x_42)) (iff x_61 x_43)) (= x_51 x_33)) $cvcl_49) $cvcl_50) (and (and (and (and (and (and (and (and (and (= x_57 1) (iff x_61 x_42)) (= ?cvcl_48 x_33)) (<= (+ ?cvcl_48 x_17) x_51)) (or (and (and (= x_62 0) $cvcl_49) $cvcl_50) (and (and (= x_62 1) (iff x_37 x_43)) (iff x_55 (not x_37))) )) (iff x_63 x_45)) (iff x_58 x_40)) (= x_64 x_46)) (= x_53 x_35)) $cvcl_51) )) (or (or (and (and (and (= x_65 0) $cvcl_57) (or (not (<= x_32 ?cvcl_53)) (iff x_63 x_37) )) $cvcl_54) (and (and (and (= x_65 1) $cvcl_52) (xor x_37 x_55 )) (= x_50 (+ ?cvcl_53 x_18))) ) (and (and (and (= x_65 2) $cvcl_52) (iff x_37 x_55)) $cvcl_54) )) (or (or (and (and (and (= x_66 0) (not $cvcl_55)) (or (not (<= x_34 ?cvcl_48)) (iff x_60 x_41) )) $cvcl_56) (and (and (and (= x_66 1) $cvcl_55) (xor x_41 x_59 )) (= x_52 (+ ?cvcl_48 x_30))) ) (and (and (and (= x_66 2) $cvcl_55) (iff x_41 x_59)) $cvcl_56) )) (or (or (and (and (and (= x_67 0) $cvcl_57) (or (not (<= x_36 ?cvcl_53)) (= x_64 x_38) )) $cvcl_59) (and (and (and (= x_67 1) $cvcl_52) (not $cvcl_58)) (= x_54 (+ ?cvcl_53 x_18))) ) (and (and (and (= x_67 2) $cvcl_52) $cvcl_58) $cvcl_59) )) (or (and (and (and (and (and (and (and (and (and (= x_39 0) (iff x_40 x_25)) (= ?cvcl_60 x_11)) (<= (+ ?cvcl_60 x_16) x_35)) (or $cvcl_63 (iff x_41 x_20) )) (iff x_42 x_22)) (iff x_43 x_23)) (= x_33 x_9)) $cvcl_61) $cvcl_62) (and (and (and (and (and (and (and (and (and (= x_39 1) (iff x_43 x_22)) (= ?cvcl_60 x_9)) (<= (+ ?cvcl_60 x_17) x_33)) (or (and (and (= x_44 0) $cvcl_61) $cvcl_62) (and (and (= x_44 1) (iff x_13 x_23)) (iff x_37 (not x_13))) )) (iff x_45 x_25)) (iff x_40 x_20)) (= x_46 x_26)) (= x_35 x_11)) $cvcl_63) )) (or (or (and (and (and (= x_47 0) $cvcl_69) (or (not (<= x_8 ?cvcl_65)) (iff x_45 x_13) )) $cvcl_66) (and (and (and (= x_47 1) $cvcl_64) (xor x_13 x_37 )) (= x_32 (+ ?cvcl_65 x_18))) ) (and (and (and (= x_47 2) $cvcl_64) (iff x_13 x_37)) $cvcl_66) )) (or (or (and (and (and (= x_48 0) (not $cvcl_67)) (or (not (<= x_10 ?cvcl_60)) (iff x_42 x_21) )) $cvcl_68) (and (and (and (= x_48 1) $cvcl_67) (xor x_21 x_41 )) (= x_34 (+ ?cvcl_60 x_30))) ) (and (and (and (= x_48 2) $cvcl_67) (iff x_21 x_41)) $cvcl_68) )) (or (or (and (and (and (= x_49 0) $cvcl_69) (or (not (<= x_12 ?cvcl_65)) (= x_46 x_14) )) $cvcl_71) (and (and (and (= x_49 1) $cvcl_64) (not $cvcl_70)) (= x_36 (+ ?cvcl_65 x_18))) ) (and (and (and (= x_49 2) $cvcl_64) $cvcl_70) $cvcl_71) )) (or (and (and (and (and (and (and (and (and (and (= x_19 0) (iff x_20 x_0)) (= ?cvcl_72 x_2)) (<= (+ ?cvcl_72 x_16) x_11)) (or $cvcl_76 (iff x_21 x_1) )) (iff x_22 x_4)) (iff x_23 x_5)) (= x_9 x_6)) $cvcl_73) $cvcl_74) (and (and (and (and (and (and (and (and (and (= x_19 1) (iff x_23 x_4)) (= ?cvcl_72 x_6)) (<= (+ ?cvcl_72 x_17) x_9)) (or (and (and (= x_24 0) $cvcl_73) $cvcl_74) (and (and (= x_24 1) (iff x_7 x_5)) (iff x_13 $cvcl_75)) )) (iff x_25 x_0)) (iff x_20 x_1)) (= x_26 x_27)) (= x_11 x_2)) $cvcl_76) )) (or (or (and (and (and (= x_28 0) $cvcl_82) (or $cvcl_83 (iff x_25 x_7) )) $cvcl_79) (and (and (and (= x_28 1) $cvcl_77) (xor x_7 x_13 )) (= x_8 (+ ?cvcl_78 x_18))) ) (and (and (and (= x_28 2) $cvcl_77) (iff x_7 x_13)) $cvcl_79) )) (or (or (and (and (and (= x_29 0) (not $cvcl_80)) (or (not (>= ?cvcl_72 0)) (iff x_22 x_3) )) $cvcl_81) (and (and (and (= x_29 1) $cvcl_80) (xor x_3 x_21 )) (= x_10 (+ ?cvcl_72 x_30))) ) (and (and (and (= x_29 2) $cvcl_80) (iff x_3 x_21)) $cvcl_81) )) (or (or (and (and (and (= x_31 0) $cvcl_82) (or $cvcl_83 (= x_26 x_15) )) $cvcl_85) (and (and (and (= x_31 1) $cvcl_77) (not $cvcl_84)) (= x_12 (+ ?cvcl_78 x_18))) ) (and (and (and (= x_31 2) $cvcl_77) $cvcl_84) $cvcl_85) )) (or (or (or (or (or (or (or (and (xor x_130 x_131 ) (not (= x_136 x_128))) (and (xor x_112 x_113 ) (not (= x_118 x_110))) ) (and (xor x_94 x_95 ) (not (= x_100 x_92))) ) (and (xor x_76 x_77 ) (not (= x_82 x_74))) ) (and (xor x_58 x_59 ) (not (= x_64 x_56))) ) (and (xor x_40 x_41 ) (not (= x_46 x_38))) ) (and (xor x_20 x_21 ) (not (= x_26 x_14))) ) (and (xor x_1 x_3 ) (not (= x_27 x_15))) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +) |