(set-option :incremental false)
(set-info :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")
(set-info :status unsat)
(set-info :category "industrial")
(set-info :difficulty "0")
(set-logic QF_LRA)
(declare-fun x_0 () Bool)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Real)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Real)
(declare-fun x_7 () Bool)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Bool)
(declare-fun x_21 () Bool)
(declare-fun x_22 () Bool)
(declare-fun x_23 () Bool)
(declare-fun x_24 () Real)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Bool)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Bool)
(declare-fun x_41 () Bool)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Bool)
(declare-fun x_44 () Real)
(declare-fun x_45 () Bool)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Real)
(declare-fun x_55 () Bool)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Bool)
(declare-fun x_59 () Bool)
(declare-fun x_60 () Bool)
(declare-fun x_61 () Bool)
(declare-fun x_62 () Real)
(declare-fun x_63 () Bool)
(declare-fun x_64 () Real)
(declare-fun x_65 () Real)
(declare-fun x_66 () Real)
(declare-fun x_67 () Real)
(declare-fun x_68 () Real)
(declare-fun x_69 () Real)
(declare-fun x_70 () Real)
(declare-fun x_71 () Real)
(declare-fun x_72 () Real)
(declare-fun x_73 () Bool)
(declare-fun x_74 () Real)
(declare-fun x_75 () Real)
(declare-fun x_76 () Bool)
(declare-fun x_77 () Bool)
(declare-fun x_78 () Bool)
(declare-fun x_79 () Bool)
(declare-fun x_80 () Real)
(declare-fun x_81 () Bool)
(declare-fun x_82 () Real)
(declare-fun x_83 () Real)
(declare-fun x_84 () Real)
(declare-fun x_85 () Real)
(declare-fun x_86 () Real)
(declare-fun x_87 () Real)
(declare-fun x_88 () Real)
(declare-fun x_89 () Real)
(declare-fun x_90 () Real)
(declare-fun x_91 () Bool)
(declare-fun x_92 () Real)
(declare-fun x_93 () Real)
(declare-fun x_94 () Bool)
(declare-fun x_95 () Bool)
(declare-fun x_96 () Bool)
(declare-fun x_97 () Bool)
(declare-fun x_98 () Real)
(declare-fun x_99 () Bool)
(declare-fun x_100 () Real)
(declare-fun x_101 () Real)
(declare-fun x_102 () Real)
(declare-fun x_103 () Real)
(declare-fun x_104 () Real)
(declare-fun x_105 () Real)
(declare-fun x_106 () Real)
(declare-fun x_107 () Real)
(declare-fun x_108 () Real)
(declare-fun x_109 () Bool)
(declare-fun x_110 () Real)
(declare-fun x_111 () Real)
(declare-fun x_112 () Bool)
(declare-fun x_113 () Bool)
(declare-fun x_114 () Bool)
(declare-fun x_115 () Bool)
(declare-fun x_116 () Real)
(declare-fun x_117 () Bool)
(declare-fun x_118 () Real)
(declare-fun x_119 () Real)
(declare-fun x_120 () Real)
(declare-fun x_121 () Real)
(declare-fun x_122 () Real)
(declare-fun x_123 () Real)
(declare-fun x_124 () Real)
(declare-fun x_125 () Real)
(declare-fun x_126 () Real)
(declare-fun x_127 () Bool)
(declare-fun x_128 () Real)
(declare-fun x_129 () Real)
(declare-fun x_130 () Bool)
(declare-fun x_131 () Bool)
(declare-fun x_132 () Bool)
(declare-fun x_133 () Bool)
(declare-fun x_134 () Real)
(declare-fun x_135 () Bool)
(declare-fun x_136 () Real)
(declare-fun x_137 () Real)
(declare-fun x_138 () Real)
(declare-fun x_139 () Real)
(check-sat-assuming ( (let ((_let_0 (= x_6 x_9))) (let ((_let_1 (= x_2 x_11))) (let ((_let_2 (not _let_1))) (let ((_let_3 (= x_13 x_7))) (let ((_let_4 (= x_14 x_15))) (let ((_let_5 (ite (<= x_6 x_2) x_6 x_2))) (let ((_let_6 (ite (<= x_2 x_6) x_2 x_6))) (let ((_let_7 (= x_32 x_8))) (let ((_let_8 (= x_9 x_33))) (let ((_let_9 (= x_34 x_10))) (let ((_let_10 (= x_11 x_35))) (let ((_let_11 (not _let_10))) (let ((_let_12 (= x_36 x_12))) (let ((_let_13 (= x_37 x_13))) (let ((_let_14 (= x_38 x_14))) (let ((_let_15 (ite (<= x_9 x_11) x_9 x_11))) (let ((_let_16 (ite (<= x_11 x_9) x_11 x_9))) (let ((_let_17 (= x_50 x_32))) (let ((_let_18 (= x_33 x_51))) (let ((_let_19 (= x_52 x_34))) (let ((_let_20 (= x_35 x_53))) (let ((_let_21 (not _let_20))) (let ((_let_22 (= x_54 x_36))) (let ((_let_23 (= x_55 x_37))) (let ((_let_24 (= x_56 x_38))) (let ((_let_25 (ite (<= x_33 x_35) x_33 x_35))) (let ((_let_26 (ite (<= x_35 x_33) x_35 x_33))) (let ((_let_27 (= x_68 x_50))) (let ((_let_28 (= x_51 x_69))) (let ((_let_29 (= x_70 x_52))) (let ((_let_30 (= x_53 x_71))) (let ((_let_31 (not _let_30))) (let ((_let_32 (= x_72 x_54))) (let ((_let_33 (= x_73 x_55))) (let ((_let_34 (= x_74 x_56))) (let ((_let_35 (ite (<= x_51 x_53) x_51 x_53))) (let ((_let_36 (ite (<= x_53 x_51) x_53 x_51))) (let ((_let_37 (= x_86 x_68))) (let ((_let_38 (= x_69 x_87))) (let ((_let_39 (= x_88 x_70))) (let ((_let_40 (= x_71 x_89))) (let ((_let_41 (not _let_40))) (let ((_let_42 (= x_90 x_72))) (let ((_let_43 (= x_91 x_73))) (let ((_let_44 (= x_92 x_74))) (let ((_let_45 (ite (<= x_69 x_71) x_69 x_71))) (let ((_let_46 (ite (<= x_71 x_69) x_71 x_69))) (let ((_let_47 (= x_104 x_86))) (let ((_let_48 (= x_87 x_105))) (let ((_let_49 (= x_106 x_88))) (let ((_let_50 (= x_89 x_107))) (let ((_let_51 (not _let_50))) (let ((_let_52 (= x_108 x_90))) (let ((_let_53 (= x_109 x_91))) (let ((_let_54 (= x_110 x_92))) (let ((_let_55 (ite (<= x_87 x_89) x_87 x_89))) (let ((_let_56 (ite (<= x_89 x_87) x_89 x_87))) (let ((_let_57 (= x_122 x_104))) (let ((_let_58 (= x_105 x_123))) (let ((_let_59 (= x_124 x_106))) (let ((_let_60 (= x_107 x_125))) (let ((_let_61 (not _let_60))) (let ((_let_62 (= x_126 x_108))) (let ((_let_63 (= x_127 x_109))) (let ((_let_64 (= x_128 x_110))) (let ((_let_65 (ite (<= x_105 x_107) x_105 x_107))) (let ((_let_66 (ite (<= x_107 x_105) x_107 x_105))) (let ((_let_67 (= x_131 x_113))) (let ((_let_68 (= x_110 x_128))) (let ((_let_69 (= x_113 x_95))) (let ((_let_70 (= x_92 x_110))) (let ((_let_71 (= x_95 x_77))) (let ((_let_72 (= x_74 x_92))) (let ((_let_73 (= x_77 x_59))) (let ((_let_74 (= x_56 x_74))) (let ((_let_75 (= x_59 x_41))) (let ((_let_76 (= x_38 x_56))) (let ((_let_77 (= x_41 x_21))) (let ((_let_78 (= x_14 x_38))) (let ((_let_79 (= x_21 x_3))) (let ((_let_80 (= x_15 x_14))) (let ((_let_81 (not (>= _let_5 0.0)))) (let ((_let_82 (= x_8 0.0))) (let ((_let_83 (= x_10 0.0))) (let ((_let_84 (= x_12 0.0))) (let ((_let_85 (+ _let_65 x_18))) (let ((_let_86 (+ _let_55 x_18))) (let ((_let_87 (+ _let_45 x_18))) (let ((_let_88 (+ _let_35 x_18))) (let ((_let_89 (+ _let_25 x_18))) (let ((_let_90 (+ _let_15 x_18))) (let ((_let_91 (+ _let_5 x_18))) (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.0) (> x_17 0.0)) (>= x_18 0.0)) (< x_18 x_16)) (< x_18 x_17)) (>= x_30 0.0)) (< x_30 x_16)) (< x_30 x_17)) (not x_0)) (not x_1)) (>= x_2 0.0)) (not x_3)) (not x_4)) (not x_5)) (>= x_6 0.0)) (not x_7)) (or (and (and (and (and (and (and (and (and (and (= x_129 0.0) (= x_130 x_117)) (= _let_66 x_107)) (<= (+ _let_66 x_16) x_125)) (or _let_67 (= x_131 x_112))) (= x_132 x_114)) (= x_133 x_115)) (= x_123 x_105)) _let_63) _let_64) (and (and (and (and (and (and (and (and (and (= x_129 1.0) (= x_133 x_114)) (= _let_66 x_105)) (<= (+ _let_66 x_17) x_123)) (or (and (and (= x_134 0.0) _let_63) _let_64) (and (and (= x_134 1.0) (= x_109 x_115)) (= x_127 (not x_109))))) (= x_135 x_117)) (= x_130 x_112)) (= x_136 x_118)) (= x_125 x_107)) _let_67))) (or (or (and (and (and (= x_137 0.0) _let_61) (or (not (<= x_104 _let_65)) (= x_135 x_109))) _let_57) (and (and (and (= x_137 1.0) _let_60) (xor x_109 x_127)) (= x_122 _let_85))) (and (and (and (= x_137 2.0) _let_60) (= x_109 x_127)) _let_57))) (or (or (and (and (and (= x_138 0.0) (not _let_58)) (or (not (<= x_106 _let_66)) (= x_132 x_113))) _let_59) (and (and (and (= x_138 1.0) _let_58) (xor x_113 x_131)) (= x_124 (+ _let_66 x_30)))) (and (and (and (= x_138 2.0) _let_58) (= x_113 x_131)) _let_59))) (or (or (and (and (and (= x_139 0.0) _let_61) (or (not (<= x_108 _let_65)) (= x_136 x_110))) _let_62) (and (and (and (= x_139 1.0) _let_60) (not _let_68)) (= x_126 _let_85))) (and (and (and (= x_139 2.0) _let_60) _let_68) _let_62))) (or (and (and (and (and (and (and (and (and (and (= x_111 0.0) (= x_112 x_99)) (= _let_56 x_89)) (<= (+ _let_56 x_16) x_107)) (or _let_69 (= x_113 x_94))) (= x_114 x_96)) (= x_115 x_97)) (= x_105 x_87)) _let_53) _let_54) (and (and (and (and (and (and (and (and (and (= x_111 1.0) (= x_115 x_96)) (= _let_56 x_87)) (<= (+ _let_56 x_17) x_105)) (or (and (and (= x_116 0.0) _let_53) _let_54) (and (and (= x_116 1.0) (= x_91 x_97)) (= x_109 (not x_91))))) (= x_117 x_99)) (= x_112 x_94)) (= x_118 x_100)) (= x_107 x_89)) _let_69))) (or (or (and (and (and (= x_119 0.0) _let_51) (or (not (<= x_86 _let_55)) (= x_117 x_91))) _let_47) (and (and (and (= x_119 1.0) _let_50) (xor x_91 x_109)) (= x_104 _let_86))) (and (and (and (= x_119 2.0) _let_50) (= x_91 x_109)) _let_47))) (or (or (and (and (and (= x_120 0.0) (not _let_48)) (or (not (<= x_88 _let_56)) (= x_114 x_95))) _let_49) (and (and (and (= x_120 1.0) _let_48) (xor x_95 x_113)) (= x_106 (+ _let_56 x_30)))) (and (and (and (= x_120 2.0) _let_48) (= x_95 x_113)) _let_49))) (or (or (and (and (and (= x_121 0.0) _let_51) (or (not (<= x_90 _let_55)) (= x_118 x_92))) _let_52) (and (and (and (= x_121 1.0) _let_50) (not _let_70)) (= x_108 _let_86))) (and (and (and (= x_121 2.0) _let_50) _let_70) _let_52))) (or (and (and (and (and (and (and (and (and (and (= x_93 0.0) (= x_94 x_81)) (= _let_46 x_71)) (<= (+ _let_46 x_16) x_89)) (or _let_71 (= x_95 x_76))) (= x_96 x_78)) (= x_97 x_79)) (= x_87 x_69)) _let_43) _let_44) (and (and (and (and (and (and (and (and (and (= x_93 1.0) (= x_97 x_78)) (= _let_46 x_69)) (<= (+ _let_46 x_17) x_87)) (or (and (and (= x_98 0.0) _let_43) _let_44) (and (and (= x_98 1.0) (= x_73 x_79)) (= x_91 (not x_73))))) (= x_99 x_81)) (= x_94 x_76)) (= x_100 x_82)) (= x_89 x_71)) _let_71))) (or (or (and (and (and (= x_101 0.0) _let_41) (or (not (<= x_68 _let_45)) (= x_99 x_73))) _let_37) (and (and (and (= x_101 1.0) _let_40) (xor x_73 x_91)) (= x_86 _let_87))) (and (and (and (= x_101 2.0) _let_40) (= x_73 x_91)) _let_37))) (or (or (and (and (and (= x_102 0.0) (not _let_38)) (or (not (<= x_70 _let_46)) (= x_96 x_77))) _let_39) (and (and (and (= x_102 1.0) _let_38) (xor x_77 x_95)) (= x_88 (+ _let_46 x_30)))) (and (and (and (= x_102 2.0) _let_38) (= x_77 x_95)) _let_39))) (or (or (and (and (and (= x_103 0.0) _let_41) (or (not (<= x_72 _let_45)) (= x_100 x_74))) _let_42) (and (and (and (= x_103 1.0) _let_40) (not _let_72)) (= x_90 _let_87))) (and (and (and (= x_103 2.0) _let_40) _let_72) _let_42))) (or (and (and (and (and (and (and (and (and (and (= x_75 0.0) (= x_76 x_63)) (= _let_36 x_53)) (<= (+ _let_36 x_16) x_71)) (or _let_73 (= x_77 x_58))) (= x_78 x_60)) (= x_79 x_61)) (= x_69 x_51)) _let_33) _let_34) (and (and (and (and (and (and (and (and (and (= x_75 1.0) (= x_79 x_60)) (= _let_36 x_51)) (<= (+ _let_36 x_17) x_69)) (or (and (and (= x_80 0.0) _let_33) _let_34) (and (and (= x_80 1.0) (= x_55 x_61)) (= x_73 (not x_55))))) (= x_81 x_63)) (= x_76 x_58)) (= x_82 x_64)) (= x_71 x_53)) _let_73))) (or (or (and (and (and (= x_83 0.0) _let_31) (or (not (<= x_50 _let_35)) (= x_81 x_55))) _let_27) (and (and (and (= x_83 1.0) _let_30) (xor x_55 x_73)) (= x_68 _let_88))) (and (and (and (= x_83 2.0) _let_30) (= x_55 x_73)) _let_27))) (or (or (and (and (and (= x_84 0.0) (not _let_28)) (or (not (<= x_52 _let_36)) (= x_78 x_59))) _let_29) (and (and (and (= x_84 1.0) _let_28) (xor x_59 x_77)) (= x_70 (+ _let_36 x_30)))) (and (and (and (= x_84 2.0) _let_28) (= x_59 x_77)) _let_29))) (or (or (and (and (and (= x_85 0.0) _let_31) (or (not (<= x_54 _let_35)) (= x_82 x_56))) _let_32) (and (and (and (= x_85 1.0) _let_30) (not _let_74)) (= x_72 _let_88))) (and (and (and (= x_85 2.0) _let_30) _let_74) _let_32))) (or (and (and (and (and (and (and (and (and (and (= x_57 0.0) (= x_58 x_45)) (= _let_26 x_35)) (<= (+ _let_26 x_16) x_53)) (or _let_75 (= x_59 x_40))) (= x_60 x_42)) (= x_61 x_43)) (= x_51 x_33)) _let_23) _let_24) (and (and (and (and (and (and (and (and (and (= x_57 1.0) (= x_61 x_42)) (= _let_26 x_33)) (<= (+ _let_26 x_17) x_51)) (or (and (and (= x_62 0.0) _let_23) _let_24) (and (and (= x_62 1.0) (= x_37 x_43)) (= x_55 (not x_37))))) (= x_63 x_45)) (= x_58 x_40)) (= x_64 x_46)) (= x_53 x_35)) _let_75))) (or (or (and (and (and (= x_65 0.0) _let_21) (or (not (<= x_32 _let_25)) (= x_63 x_37))) _let_17) (and (and (and (= x_65 1.0) _let_20) (xor x_37 x_55)) (= x_50 _let_89))) (and (and (and (= x_65 2.0) _let_20) (= x_37 x_55)) _let_17))) (or (or (and (and (and (= x_66 0.0) (not _let_18)) (or (not (<= x_34 _let_26)) (= x_60 x_41))) _let_19) (and (and (and (= x_66 1.0) _let_18) (xor x_41 x_59)) (= x_52 (+ _let_26 x_30)))) (and (and (and (= x_66 2.0) _let_18) (= x_41 x_59)) _let_19))) (or (or (and (and (and (= x_67 0.0) _let_21) (or (not (<= x_36 _let_25)) (= x_64 x_38))) _let_22) (and (and (and (= x_67 1.0) _let_20) (not _let_76)) (= x_54 _let_89))) (and (and (and (= x_67 2.0) _let_20) _let_76) _let_22))) (or (and (and (and (and (and (and (and (and (and (= x_39 0.0) (= x_40 x_25)) (= _let_16 x_11)) (<= (+ _let_16 x_16) x_35)) (or _let_77 (= x_41 x_20))) (= x_42 x_22)) (= x_43 x_23)) (= x_33 x_9)) _let_13) _let_14) (and (and (and (and (and (and (and (and (and (= x_39 1.0) (= x_43 x_22)) (= _let_16 x_9)) (<= (+ _let_16 x_17) x_33)) (or (and (and (= x_44 0.0) _let_13) _let_14) (and (and (= x_44 1.0) (= x_13 x_23)) (= x_37 (not x_13))))) (= x_45 x_25)) (= x_40 x_20)) (= x_46 x_26)) (= x_35 x_11)) _let_77))) (or (or (and (and (and (= x_47 0.0) _let_11) (or (not (<= x_8 _let_15)) (= x_45 x_13))) _let_7) (and (and (and (= x_47 1.0) _let_10) (xor x_13 x_37)) (= x_32 _let_90))) (and (and (and (= x_47 2.0) _let_10) (= x_13 x_37)) _let_7))) (or (or (and (and (and (= x_48 0.0) (not _let_8)) (or (not (<= x_10 _let_16)) (= x_42 x_21))) _let_9) (and (and (and (= x_48 1.0) _let_8) (xor x_21 x_41)) (= x_34 (+ _let_16 x_30)))) (and (and (and (= x_48 2.0) _let_8) (= x_21 x_41)) _let_9))) (or (or (and (and (and (= x_49 0.0) _let_11) (or (not (<= x_12 _let_15)) (= x_46 x_14))) _let_12) (and (and (and (= x_49 1.0) _let_10) (not _let_78)) (= x_36 _let_90))) (and (and (and (= x_49 2.0) _let_10) _let_78) _let_12))) (or (and (and (and (and (and (and (and (and (and (= x_19 0.0) (= x_20 x_0)) (= _let_6 x_2)) (<= (+ _let_6 x_16) x_11)) (or _let_79 (= x_21 x_1))) (= x_22 x_4)) (= x_23 x_5)) (= x_9 x_6)) _let_3) _let_4) (and (and (and (and (and (and (and (and (and (= x_19 1.0) (= x_23 x_4)) (= _let_6 x_6)) (<= (+ _let_6 x_17) x_9)) (or (and (and (= x_24 0.0) _let_3) _let_4) (and (and (= x_24 1.0) (= x_7 x_5)) (= x_13 (not x_7))))) (= x_25 x_0)) (= x_20 x_1)) (= x_26 x_27)) (= x_11 x_2)) _let_79))) (or (or (and (and (and (= x_28 0.0) _let_2) (or _let_81 (= x_25 x_7))) _let_82) (and (and (and (= x_28 1.0) _let_1) (xor x_7 x_13)) (= x_8 _let_91))) (and (and (and (= x_28 2.0) _let_1) (= x_7 x_13)) _let_82))) (or (or (and (and (and (= x_29 0.0) (not _let_0)) (or (not (>= _let_6 0.0)) (= x_22 x_3))) _let_83) (and (and (and (= x_29 1.0) _let_0) (xor x_3 x_21)) (= x_10 (+ _let_6 x_30)))) (and (and (and (= x_29 2.0) _let_0) (= x_3 x_21)) _let_83))) (or (or (and (and (and (= x_31 0.0) _let_2) (or _let_81 (= x_26 x_15))) _let_84) (and (and (and (= x_31 1.0) _let_1) (not _let_80)) (= x_12 _let_91))) (and (and (and (= x_31 2.0) _let_1) _let_80) _let_84))) (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))