Hanging

let rec appendo a b ab =
  conde
    [ ((a === nil ()) &&& (b === ab))
    ; fresh (h t ab')
        (a === h%t)
        (h%ab' === ab)
        (appendo t b ab')
    ]

let rec reverso a b =
  conde
    [ ((a === nil ()) &&& (b === nil ()))
    ; fresh (h t a')
        (a === h%t)
        (reverso t a')
        (appendo a' !<h b)
    ]

let _ =
  (* OK *)
  run_exn show_int_list (-1)q qh (REPR (fun q   -> reverso   (ilist [1; 2; 3; 4]) q             ));
  (* Hangs *)
  run_exn show_int_list (-1)q qh (REPR (fun q   -> reverso q (ilist [1; 2; 3; 4])               ))

let rec reverso a b =
  conde
    [ ((a === nil ()) &&& (b === nil ()))
    ; fresh (h t a')
        (a === h%t)
        (appendo a' !<h b)
        (reverso t a')
    ]

let _ =
  (* OK *)
  run_exn show_int_list (-1)q qh (REPR (fun q   -> reverso q (ilist [1; 2; 3; 4])               ))
  (* Hangs *)
  run_exn show_int_list (-1)q qh (REPR (fun q   -> reverso   (ilist [1; 2; 3; 4]) q             ));