Project

General

Profile

Revision f133f964

View differences:

src/backends/Horn/horn_backend.ml
353 353
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
354 354
            (* print_string pp_val; *)
355 355
            let instrs_concat = m.mstep.step_instrs in
356
            Format.fprintf fmt "; With Asserts @.";
357
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
356
            Format.fprintf fmt "; with Invariants @.";
357
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
358 358
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
359
                           (pp_conj pp_val) assertsl
359 360
                           pp_machine_step_name m.mname.node_id
360 361
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
361
	    Format.fprintf fmt " @[<v 2>%a@]@ @.@.@."
362
	                   (pp_conj pp_val) assertsl;
362

  
363

  
364
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
365
            (*                 (pp_conj pp_val) assertsl; *)
366

  
363 367
          end
364 368
       );
365 369

  

Also available in: Unified diff