anchor.diff:  let mkImplies (ctx: Z3.Context) l r =
       (* l => r <-> ¬l v r.
        * This implies (excuse the pun) that l false or r true will
  -     * make the expression a tautology.
  +     * make the expression a tautology;
  +     * similarly, l true yields r, and r false yields ¬l.
        *)
       match l, r with
       | (ZFalse, _) | (_, ZTrue) -> ctx.MkTrue ()
  
positive.code: 
  let mkNot (ctx: Z3.Context) x =
      match x with
      | ZFalse -> ctx.MkTrue ()
      | ZTrue -> ctx.MkFalse ()
      | _ -> ctx.MkNot x
  
negative.code:     else
          let cs = conjuncts |> Seq.filter (fun (x: Z3.BoolExpr) -> not x.IsTrue) |> Array.ofSeq
          match cs with
          // True is the zero of and.
          | [||] -> ctx.MkTrue ()
          | [| x |] -> x
          | xs -> ctx.MkAnd (xs)
  