Project

General

Profile

Revision ef598ac3 src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
165 165
        if Z3.Expr.is_numeral ze then
166 166
          let e =
167 167
            if Z3.Arithmetic.is_real ze then
168
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
169 168
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
169
              (* Use to return a Num.ratio. Now Q.t *)
170
              let ratio = Z3.Arithmetic.Real.get_ratio ze in
171
              (*let num =  Num.num_of_ratio ratio in
172
              let real = Real.create_num num s in*)
173
              let real = Real.create_q ratio s in
170 174
              mkexpr
171 175
                Location.dummy_loc
172 176
                (Expr_const
173
                   (Const_real
174
                      (Real.create_num num s)))
177
                   (Const_real real))
175 178
            else if Z3.Arithmetic.is_int ze then
176 179
              mkexpr
177 180
                Location.dummy_loc
178 181
                (Expr_const
179
                   (Const_int
180
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
182
                   (Const_int 
183
                      (Z.to_int (Z3.Arithmetic.Integer.get_big_int ze))))
181 184
            else if Z3.Expr.is_const ze then
182 185
              match Z3.Expr.to_string ze with
183 186
              | "true" -> mkexpr Location.dummy_loc

Also available in: Unified diff