Project

General

Profile

Revision 8d0c1f8e

View differences:

src/backends/Horn/horn_backend_printers.ml
252 252
       statement. *)
253 253
    let self = m.mname.node_id in
254 254
    let pp_branch fmt (tag, instrs) =
255
      fprintf fmt "@[<v 3>(=> (= %a %s)@ "
255
      fprintf fmt 
256
	"@[<v 3>(or (not (= %a %s))@ " 
257
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
258
					  seems that => within Horn predicate
259
					  may cause trouble. I have hard time
260
					  producing a MWE, so I'll just keep the
261
					  fix here as (not a) or b *)
256 262
	(pp_horn_val self (pp_horn_var m)) g
257 263
	tag;
258 264
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
......
420 426

  
421 427

  
422 428
(* Local Variables: *)
423
(* compile-command:"make -C ../.." *)
429
(* compile-command:"make -C ../../.." *)
424 430
(* End: *)

Also available in: Unified diff