/src/tools/zustre/zustre_common.ml - Diff - LustreC

« Previous | Next »

Revision 58301109

Added by Pierre-Loïc Garoche almost 3 years ago

ID 5830110920194b20d9d29d11c90529d4758cd7a8
Parent 2104c80a
Child 7aaacbc9

Zustre: Bug solved in const injection for reals

     let rec horn_const_to_expr c =
       match c with
         | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
         | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
         | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_s !ctx s
         | Const_tag t    -> horn_tag_to_expr t
         | _              -> assert false

Also available in: Unified diff