anchor.diff:      function
       | BEq (Bool x, Bool y) -> Some (x, y)
       | _ -> None
  +
  +
  +/// Define when two Boolean expressions are trivially equal 
  +/// Eg: (= a b)  is equivalent ot (=b a)
  +let rec eqBoolExpr (e1: BoolExpr<'var>) (e2:BoolExpr<'var>) : bool   = 
  +  match e1, e2 with 
  +  | BEq (a1,a2), BEq (b1,b2) -> 
  +     ((a1=a2 && b1=b2) || (a1=b2 && b1=a2))
  +  | BNot a, BNot b -> eqBoolExpr a b 
  +  | _ -> false 
  +
  +
  +/// Remove duplicate boolean expressions 
  +/// TODO(@septract) This is stupid, should do it more cleverly 
  +let rec remExprDup (xs: List<BoolExpr<'var>>) : List<BoolExpr<'var>> =   
  +  match xs with 
  +  | (x::xs) -> 
  +      let xs2 = remExprDup xs in 
  +      if (List.exists (eqBoolExpr x) xs) then xs2 else x::xs2
  +  | x -> x 
  +
   
   /// Recursively simplify a formula
   /// Note: this does _not_ simplify variables.
  
positive.code:         | BLt of IntExpr<'var> * IntExpr<'var>
          | BNot of BoolExpr<'var>
          override this.ToString () = sprintf "%A" this
  
      /// Type for fresh variable generators.
      type FreshGen = bigint ref
  
negative.code:     /// <typeparam name="var">
      ///     The type of variables in the expression.
      /// </typeparam>
      
      type Expr<'var> = Typed<IntExpr<'var>, BoolExpr<'var>>
  
      /// <summary>
  