Revision 8d0c1f8e
Added by Pierre-Loïc Garoche almost 9 years ago
| 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
fixed a z3 bug for => within Horn clauses