anchor.diff:          printBoolExpr (printSym printMarkedVar) a 
   
       let findVarsGrass (zterm : Backends.Z3.Types.ZTerm) : seq<MarkedVar> = 
  +        // TODO @(septract) Should this conjoin the command as well? 
           BAnd [zterm.SymBool.WPre; zterm.SymBool.Goal] 
           |> findMarkedVars (tliftToBoolSrc (tliftToExprDest collectSymMarkedVars)) 
           |> lift (Set.map valueOf) 
  
positive.code:                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" 
  
  
negative.code:     open Starling.Core.Model.Pretty
      open Starling.Core.Symbolic.Pretty
  
      /// Prints a marked Var 
      let printMarkedVar (v : MarkedVar) : Doc =
          match v with 
          | Before s -> String "before_" <-> String s 
  