--- a/trunk/Toss/Formula/BoolFormula.ml
+++ b/trunk/Toss/Formula/BoolFormula.ml
@@ -1205,6 +1205,8 @@
     | _ -> failwith "get_lit: not a literal" in
   let rec print_qrec phi = match phi.x with
     | QVar _ | QNot _ -> failwith "print_qpro: error - var or negation"
+    | QAnd [] -> "d\n1\n1\n/d"
+    | QOr [] -> "c\n1\n1\n/c"
     | QAnd l -> 
       let (lits, other) = List.partition is_lit l in
       let lits = List.rev_map get_lit lits in
@@ -1227,6 +1229,7 @@
         Printf.sprintf "d\n%s\n%s\n%s\n/d" pos_s neg_s oth_s
     | QEx (vs, ({x=QVar _} as f)) -> print_qrec (cEx (vs, cAnd [f]))
     | QEx (vs, ({x=QNot _} as f)) -> print_qrec (cEx (vs, cAnd [f]))
+    | QEx ([], f) | QAll ([], f) -> print_qrec f
     | QEx (vs, f) -> 
       let vs_s = String.concat " " (List.map string_of_int vs) in
       Printf.sprintf "q\ne %s\n%s\n/q" vs_s (print_qrec f)
@@ -1257,6 +1260,10 @@
     | QVar v -> lp_var_truth v
     | QNot ({x=QVar v}) -> lp_var_truth (-v)
     | QNot _ -> failwith "print_lparse: error - not in nnf"
+    | QAnd [] | QOr [] -> 
+      let left = expr_id () in
+      rules := (left) :: !rules;
+      left
     | QAnd l -> 
       let left, l_ids = expr_id (), List.rev_map print_lprec l in
       rules := (left ^ " :- " ^ (String.concat ", " l_ids)) :: !rules;