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:         |> lift (Set.map valueOf >> Set.toSeq) 
          |> returnOrFail
  
      /// Add a spatial frame if an expression isn't symbolic
      // TODO @(septract) this is extremely naive at the moment. 
      let makeFrame b = 
          let exprdoc = 
             printBoolExprG (printSymGrass printMarkedVarGrass) b 
          match b with 
          | BVar (Sym s) -> exprdoc 
          | _ ->  String "sTrue() &*&" <+> exprdoc  |>  parened 
  
      /// Print top-level requires / ensures clauses 
      let printConstrGrass (s : Doc) (b : BoolExpr<Sym<MarkedVar>>) : Doc = 
          match b with 
          | BAnd xs ->  
                Seq.map makeFrame xs 
                |> Seq.map (hsep2 Nop s) 
                |> vsep 
          | x -> makeFrame x 
                 |> hsep2 Nop s
  
      /// Print a single Grasshopper query from a ZTerm 
      let printZTermGrass (svars : VarMap) 
  
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> = 
  