anchor.diff:              parened
                   (printInterpolatedSymbolicSentence pArg ws xs)
   
  -    let printExprGrass a = 
  +    let printExprGrass (a : BoolExpr<Sym<MarkedVar>>) : Doc  = 
           printBoolExpr (printSym printMarkedVar) a 
   
  -    let printQuery (zterm : Backends.Z3.Types.ZTerm) : Doc = 
  -        headed "Grasshopper terms" <| 
  -          [ printTerm
  -              (Core.Expr.Pretty.printBoolExpr (printSym printMarkedVar)) 
  -              printExprGrass 
  -              printExprGrass 
  -              zterm.SymBool ]
  +    let findVarsGrass (zterm : Backends.Z3.Types.ZTerm) : seq<MarkedVar> = 
  +        BAnd [zterm.SymBool.WPre; zterm.SymBool.Goal] 
  +        |> findMarkedVars (tliftToBoolSrc (tliftToExprDest collectSymMarkedVars)) 
  +        |> lift (Set.map valueOf) 
  +        |> lift (Set.toSeq) 
  +        |> returnOrFail
  +
  +    let printQuery (zterm: Backends.Z3.Types.ZTerm) : Doc =
  +        let varprint = Seq.map printMarkedVar (findVarsGrass zterm) 
  +                       |> (fun x -> VSep(x,String ",")) 
  +                       |> Indent 
  +        let wpreprint = zterm.SymBool.WPre 
  +                        |> printExprGrass 
  +        let goalprint = zterm.SymBool.Goal 
  +                        |> printExprGrass 
  +        let cmdprint = zterm.SymBool.Cmd 
  +                       |> (Core.Expr.Pretty.printBoolExpr (printSym printMarkedVar))
  +        vsep [ String "procedure test" <+> (varprint |> parened) 
  +               String "requires" 
  +               Indent wpreprint <+> String ";" 
  +               String "ensures" 
  +               Indent goalprint <+> String ";" 
  +               String "{}"   
  +               headed "Command" (cmdprint |> Seq.singleton)
  +             ]  
  +
  +
  +    // let printQuery (zterm : Backends.Z3.Types.ZTerm) : Doc = 
  +    //    vsep  
  +    //        [ headed "Variables" <|
  +    //              List.map printMarkedVar (findVarsGrass zterm)
  +    //          headed "Grasshopper terms" <| 
  +    //              [ printTerm
  +    //                  (Core.Expr.Pretty.printBoolExpr (printSym printMarkedVar)) 
  +    //                  printExprGrass 
  +    //                  printExprGrass 
  +    //                  zterm.SymBool ]
  +    //        ]
   
       let printGrassError e = 
           failwith "not implemented yet" 
  
positive.code:     open Starling.Core.Model.Pretty
      open Starling.Core.Symbolic.Pretty
  
      let printMarkedVar =
          function
          | Before s -> String "before_" <-> String s 
          | After s -> String "after_" <-> String s
          | Intermediate (i, s) -> String "inter_" <-> String (sprintf "%A_" i) <-> String s 
  
negative.code: open Starling.Core.Symbolic
  open Starling.Core.Instantiate
  open Starling.Core.GuardedView
  open Starling.Core.Traversal
  
  [<AutoOpen>] 
  module Types =
      type Grass = Backends.Z3.Types.ZModel // Just piggyback on Z3 model for now.  
      type Error = unit 
  
  module Pretty = 
  