Project

General

Profile

Revision cd6efd9b src/horn_backend.ml

View differences:

src/horn_backend.ml
11 11
  match (Types.repr t).Types.tdesc with
12 12
  | Types.Tbool           -> Format.fprintf fmt "Bool"
13 13
  | Types.Tint            -> Format.fprintf fmt "Int"
14
  | Types.Treal           -> Format.fprintf fmt "Real"
14 15
  | Types.Tclock _
15 16
  | Types.Tarray _
16 17
  | Types.Tstatic _
......
314 315
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
315 316

  
316 317
    Format.fprintf fmt "; Inductive def@.";
317
    Format.fprintf fmt "(declare-var dummy Bool)@.";
318 318
    Format.fprintf fmt 
319
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
319
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
320 320
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
321 321
      node
322 322
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)

Also available in: Unified diff