anchor.diff:          let cmdprint = zterm.SymBool.Cmd 
                          |> (Core.Expr.Pretty.printBoolExpr (printSymGrass printMarkedVarGrass))
           vsep [ String "procedure" <+> String name <+> (varprint |> parened) 
  -               String "requires" 
  -               Indent wpreprint <+> String ";" 
  -               String "ensures" 
  -               Indent goalprint <+> String ";" 
  +               // String "requires" 
  +               (printConstrGrass (String "requires ") zterm.SymBool.WPre) 
  +               (printConstrGrass (String "ensures  ") zterm.SymBool.Goal) 
  +               // String "ensures" 
  +               // Indent goalprint <+> String ";" 
                  cmdprint 
                       |> ssurround "/*" "*/" 
                       |> Indent |> braced 
                ]  
   
  -    /// Print all the Grasshopper queries for a model.      
  +    /// Print all the Grasshopper queries that haven't been eliminated by Z3.      
       let printQuery (model: GrassModel) : Doc = 
  -        Map.toSeq model.Axioms 
  +        let fails = extractFailures model 
  +        Map.toSeq fails 
           |> Seq.map (fun (name,term) -> printZTermGrass model.SharedVars name term) 
           |> vsep
   
  
positive.code:         |> findMarkedVars (tliftToBoolSrc (tliftToExprDest collectSymMarkedVars)) 
          |> lift (Set.map valueOf >> Set.toSeq) 
          |> returnOrFail
  
      /// Print a single Grasshopper query from a ZTerm 
      let printZTermGrass (svars : VarMap) 
  
negative.code: open Starling.Core.Instantiate
  open Starling.Core.GuardedView
  open Starling.Core.Traversal
  open Starling.Backends.Z3
  
  [<AutoOpen>] 
  module Types =
  