anchor.diff:  open Starling.Core.Expr
   open Starling.Core.Model
   open Starling.Core.Symbolic
  +open Starling.Core.Symbolic.Traversal
   open Starling.Core.Instantiate
   open Starling.Core.GuardedView
   open Starling.Core.Traversal
   open Starling.Backends.Z3
  +open Starling.Optimiser.Graph
   
   [<AutoOpen>] 
   module Types =
  
positive.code: 
          /// Print the requires / ensures clauses 
          let wpreprint = zterm.SymBool.WPre 
                          |> printBoolExprG (printSymGrass printMarkedVarGrass) 
          let goalprint = zterm.SymBool.Goal 
                          |> printBoolExprG (printSymGrass printMarkedVarGrass) 
  
          // TODO @(septract) print command properly 
          let cmdprint = zterm.SymBool.Cmd 
                         |> (Core.Expr.Pretty.printBoolExpr (printSymGrass printMarkedVarGrass))
          vsep [ String "procedure" <+> String name <+> (varprint |> parened) 
                 // String "requires" 
                 (printConstrGrass (String "requires ") zterm.SymBool.WPre) 
                 (printConstrGrass (String "ensures  ") zterm.SymBool.Goal) 
                 // String "ensures" 
                 // Indent goalprint <+> String ";" 
                 cmdprint 
                      |> ssurround "/*" "*/" 
                      |> Indent |> braced 
  
negative.code:         match v with 
          | Int name -> String name  
          | Bool name -> String name  
          | _ -> failwith "[printTypedVarGrass] Case unimplemented for Grasshopper backend." 
  
      /// Pretty-prints an arithmetic expression.
      let rec printIntExprG (pVar : 'Var -> Doc) : IntExpr<'Var> -> Doc =
          function
          | IVar c -> pVar c
          | _ -> failwith "[printIntExprG] Case unimplemented for Grasshopper backend." 
  
      /// Pretty-prints a Boolean expression.
      and printBoolExprG (pVar : Sym<MarkedVar> -> Doc) (fr : bool) (b : BoolExpr<Sym<MarkedVar>>) : Doc =
          match b, fr with 
          | NoSym x, true ->   
             String "sTrue() &*& " <+> printBoolExprG pVar false b |> parened 
          | _ -> 
             match b with 
             | BVar c -> pVar c
             | BAnd xs -> infexprV "&&" (printBoolExprG pVar fr) xs 
             | BOr xs -> infexprV "||" (printBoolExprG pVar fr) xs
             | BImplies (x, y) -> 
                 /// Convert implications to disjunctive form
                 printBoolExprG pVar fr (BOr [BNot x; y]) 
             | BNot (BEq (x, y)) -> infexpr "!=" (printExprG pVar fr) [x; y]
             | BNot x -> String "~" <+> (printBoolExprG pVar fr x) |> parened 
             | BEq (x, y) -> infexpr "==" (printExprG pVar fr) [x; y]
             | BGt (x, y) -> infexpr ">" (printIntExprG pVar) [x; y]
             | BLt (x, y) -> infexpr "<" (printIntExprG pVar) [x; y]
             | _ -> failwith "[printBoolExprG] Case unimplemented for Grasshopper backend."  
         
      /// Pretty-prints an expression.
      and printExprG (pVar : Sym<MarkedVar> -> Doc) (fr : bool) (b : Expr<Sym<MarkedVar>>) : Doc =
          match b with 
          | Int i -> printIntExprG pVar i
          | Bool b -> printBoolExprG pVar fr b
          | _ -> failwith "[printExprG] Case unimplemented for Grasshopper backend." 
  
      /// Pretty-prints a symbolic sentence 
      let rec printSymGrass (pReg : MarkedVar -> Doc) (sym : Sym<MarkedVar>) : Doc =
          match sym with
          | Reg r -> pReg r
          | Sym { Sentence = ws; Args = xs } ->
              let pArg = printExprG (printSym pReg) false
              printInterpolatedSymbolicSentence pArg ws xs
              |> parened 
  
      /// Get the set of accessed variables. 
      let findVarsGrass (zterm : Backends.Z3.Types.ZTerm) : seq<MarkedVar> = 
  