[printers] Ensure goal is in cnf before negating and printing it.

src/printers/vnnlib.ml

@@ -476,6 +476,10 @@ let print_prop_decl info fmt prop_kind pr t =
   | Decl.Plemma -> assert false
   | Decl.Paxiom -> print_axiom info fmt (pr, t)
   | Decl.Pgoal ->
+    let t =
+      (* Before negating the formula, make it in conjunctive normal form. *)
+      Why3.Split_goal.split_pos_full t |> Why3.Term.t_and_l
+    in
     let negated_term = negate_term info t in
     print_goal info fmt (pr, negated_term)