anchor.diff:          | ([], _) -> ()
           in
         ps.PrintLine "=";
  -      ps.PrintLine ("if " + (string_of_exp e) + " then");
  +      ps.PrintLine ("if " + (string_of_exp90 e) + " then");
         ps.Indent ();
         ps.PrintLine ("let " + (string_of_outs_formals outs) + " =");
         emit_block ps "" outs ss;
  
positive.code:     | EString s -> ("\"" + s.Replace("\\", "\\\\") + "\"", 99)
      | EOp (Uop (UCall CallGhost), [e]) -> (r prec e, prec)
      | EOp (Uop UReveal, [EApply (x, _, es)]) -> (r prec (vaApp "reveal_opaque" [eapply (transparent_id x) es]), prec)
      | EOp (Uop UReveal, [EVar x]) -> ("(reveal_opaque " + (sid x) + ")", prec)
      | EOp (Uop (UNot BpBool), [e]) -> ("not " + (r 99 e), 90)
      | EOp (Uop (UNot BpProp), [e]) -> ("~" + (r 99 e), 90)
      | EOp (Uop UNeg, [e]) -> ("-" + (r 99 e), 0)
  
negative.code:     | EOp (Subscript, [e1; e2]) -> (r prec (vaApp "subscript" [e1; e2]), prec)
      | EOp (Update, [e1; e2; e3]) -> (r prec (vaApp "update" [e1; e2; e3]), prec)
      | EOp (Cond, [e1; e2; e3]) -> ("if " + (r 90 e1) + " then " + (r 90 e2) + " else " + (r 90 e3), 0)
      | EOp (FieldOp x, [e]) -> ((r 95 e) + "." + (sid x), 95)
      | EOp (FieldUpdate x, [e1; e2]) -> ("({" + (r 90 e1) + " with " + (sid x) + " = " + (r 90 e2) + "})", 90)
      | EOp ((Subscript | Update | Cond | FieldOp _ | FieldUpdate _ | CodeLemmaOp | RefineOp | StateOp _ | OperandArg _), _) -> internalErr (sprintf "EOp: %A" e)
      | EApply (x, _, es) -> ((sid x) + " " + (string_of_args es), 90)
      | EBind ((Forall | Exists | Lambda), [], [], _, e) -> (r prec e, prec)
      | EBind (Forall, [], xs, ts, e) -> qbind "forall" " . " xs ts e
      | EBind (Exists, [], xs, ts, e) -> qbind "exists" " . " xs ts e
  