Project

General

Profile

Revision 58301109

View differences:

src/tools/zustre/zustre_common.ml
215 215
let rec horn_const_to_expr c =
216 216
  match c with
217 217
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
218
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
218
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_s !ctx s
219 219
    | Const_tag t    -> horn_tag_to_expr t
220 220
    | _              -> assert false
221 221

  

Also available in: Unified diff