diff --git a/col/src/main/java/vct/col/ast/print/AbstractPrinter.java b/col/src/main/java/vct/col/ast/print/AbstractPrinter.java
index ec7dae83ab..91baad9a6d 100644
--- a/col/src/main/java/vct/col/ast/print/AbstractPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/AbstractPrinter.java
@@ -65,7 +65,6 @@ public void pre_visit(ASTNode node){
     }
     Origin o=node.getOrigin();
     if (o==null){
-      //throw new Error("found "+node.getClass()+" without origin");
       o=missing;
     }
     out.enter(node.getOrigin());
@@ -153,7 +152,6 @@ public void visit(NameExpression e){
   }
 
   public void visit(MethodInvokation e){
-    //boolean statement=!in_expr;
     setExpr();
     if (e.object()!=null) {
       // TODO: manage precedence properly.
diff --git a/col/src/main/java/vct/col/ast/print/CPrinter.java b/col/src/main/java/vct/col/ast/print/CPrinter.java
index 4b86863710..7943090a20 100644
--- a/col/src/main/java/vct/col/ast/print/CPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/CPrinter.java
@@ -31,7 +31,6 @@ public void pre_visit(ASTNode node) {
 			nextExpr();
 			lbl.accept(this);
 			out.printf(":");
-			// out.printf("[");
 		}
 	}
 	
@@ -53,10 +52,7 @@ public void visit(PrimitiveType t){
 	}
 	
 	public void visit(ASTClass cl){
-		//if (cl.getDynamicCount()>0) {
-		//	Fail("dynamic entries are illegal in C");
-		//}
-    for(ASTNode item:cl.dynamicMembers()){
+		for(ASTNode item:cl.dynamicMembers()){
       item.accept(this);
     }
     for(ASTNode item:cl.staticMembers()){
@@ -97,7 +93,7 @@ public void visit(Contract c){
 	}
 	public void visit(Method m){
 	  Contract c=m.getContract();
-	  if (c!=null) visit(c); //c.accept(this);
+	  if (c!=null) visit(c);
 		nextExpr();
 		m.getReturnType().accept(this);
 		out.printf(" %s(",m.getName());
@@ -161,17 +157,7 @@ public void visit(LoopStatement l){
 	    super.visit(l);
 	  }
 	}
-	
-/*
- 	public void visit(ConstantExpression ce){
-    if (ce.value instanceof StringValue){
-      out.print("\""+org.apache.commons.lang3.StringEscapeUtils.escapeJava(ce.toString())+"\"");
-    } else {
-      out.print(ce.toString());
-    }
-  }
-*/
-	
+
 	public void visit(ReturnStatement s){
 		if (s.getExpression()==null){
 			out.printf("return");
diff --git a/col/src/main/java/vct/col/ast/print/JavaPrinter.java b/col/src/main/java/vct/col/ast/print/JavaPrinter.java
index 67ab8072b2..ea18374842 100644
--- a/col/src/main/java/vct/col/ast/print/JavaPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/JavaPrinter.java
@@ -54,7 +54,6 @@ public void pre_visit(ASTNode node){
       nextExpr();
       lbl.accept(this);
       out.printf(":");
-      //out.printf("[");
     }
     if (node.annotated()) for(ASTNode ann:node.annotations()) {
       if (ann==null){
@@ -303,12 +302,10 @@ public void visit(ASTSpecial s){
     case Goto:
       out.print("goto ");
       s.args[0].accept(this);
-      //out.println(";");
       break;
     case Label:
       out.print("label ");
       s.args[0].accept(this);
-      //out.println(";");
       break;
     case With:
       out.print("WITH");
@@ -616,7 +613,6 @@ public void visit(ASTClass cl){
     for(ASTNode item:cl){
       if (item.isStatic()){
         if (item instanceof DeclarationStatement) out.printf("static ");
-        // else out.println("/* static */");
       }
       item.accept(this);
       out.println("");
@@ -788,37 +784,6 @@ private void visitVeriFast(Contract contract) {
   }
 
   public void visit(IfStatement s){
-    /* CaseSet conflicts with send/recv in ghost mode! 
-    if (s.isValidFlag(ASTNode.GHOST) && s.getFlag(ASTNode.GHOST)){
-      int N=s.getCount();
-      out.printf ("/*@ CaseSet[");
-      for(int i=0;i<N;i++){
-        if (i>0) out.printf ("  @         ");
-        out.printf("(");
-        nextExpr();
-        s.getGuard(i).accept(this);
-        out.printf(",");
-        ASTNode n=s.getStatement(i);
-        if (n instanceof BlockStatement){
-          BlockStatement block=(BlockStatement)n;
-          int M=block.getLength();
-          for(int j=0;j<M;j++){
-            if(j>0) out.printf(";");
-            nextExpr();
-            block.getStatement(j).accept(this);
-          }
-        } else {
-          Abort("statement in caseset is not a block at %s",n.getOrigin());
-        }
-        out.printf(")");
-        if(i==N-1){
-          out.lnprintf("];");
-        } else {
-          out.lnprintf(",");
-        }
-      }
-      out.lnprintf("  @ * /");
-    } else {*/
       int N=s.getCount();
       out.printf("if (");
       nextExpr();
@@ -845,7 +810,6 @@ public void visit(IfStatement s){
           out.lnprintf(";");
         }        
       }
-    //}
   }
 
   private boolean self_terminating(ASTNode s) {
@@ -1125,18 +1089,6 @@ public void visit(MethodInvokation s){
     } else {
       super.visit(s);
     }
-    //if (s.get_before()!=null){
-    //  out.printf("/*@ ");
-    //  out.printf("with ");
-    //  s.get_before().accept(this);
-    //  out.printf(" */");
-    //}
-    //if (s.get_after()!=null){
-    //  out.printf("/*@ ");
-    //  out.printf("then ");
-    //  s.get_after().accept(this);
-    //  out.printf(" */");
-    //}    
   }
 
 
@@ -1361,7 +1313,6 @@ public void visit(ParallelRegion region){
   }
   
   public void visit(ConstantExpression ce){
-    //if (!in_expr) Abort("constant %s outside of expression for %s",ce,ce.getOrigin());
     if (ce.value() instanceof StringValue){
       out.print("\""+StringEscapeUtils.escapeJava(ce.toString())+"\"");
     } else {
diff --git a/col/src/main/java/vct/col/ast/print/PVLPrinter.java b/col/src/main/java/vct/col/ast/print/PVLPrinter.java
index 8a794dc4f2..f7230163b9 100644
--- a/col/src/main/java/vct/col/ast/print/PVLPrinter.java
+++ b/col/src/main/java/vct/col/ast/print/PVLPrinter.java
@@ -45,7 +45,6 @@ public void pre_visit(ASTNode node){
             nextExpr();
             lbl.accept(this);
             out.printf(":");
-            //out.printf("[");
         }
         if (node.annotated()) for(ASTNode ann:node.annotations()) {
             if (ann==null){
@@ -296,12 +295,10 @@ public void visit(ASTSpecial s){
             case Goto:
                 out.print("goto ");
                 s.args[0].accept(this);
-                //out.println(";");
                 break;
             case Label:
                 out.print("label ");
                 s.args[0].accept(this);
-                //out.println(";");
                 break;
             case With:
                 out.print("WITH");
@@ -568,7 +565,6 @@ public void visit(ASTClass cl){
             }
             if (item.isStatic()){
                 if (item instanceof DeclarationStatement) out.printf("static ");
-                // else out.println("/* static */");
             }
             item.accept(this);
             out.println("");
@@ -648,9 +644,7 @@ public void visit(Method m){
         if (m.getKind()==Method.Kind.Pure){
             out.printf("pure ");
         }
-        if (m.getKind()==Method.Kind.Constructor){
-            // out.printf("/*constructor*/ ");
-        } else {
+        if (m.getKind()!=Method.Kind.Constructor){
             result_type.accept(this);
             out.printf(" ");
         }
@@ -728,7 +722,6 @@ public void visit(IfStatement s){
                 out.lnprintf(";");
             }
         }
-        //}
     }
 
     private boolean self_terminating(ASTNode s) {
diff --git a/col/src/main/java/vct/col/ast/stmt/decl/NameSpace.java b/col/src/main/java/vct/col/ast/stmt/decl/NameSpace.java
index 5d2703af14..b11c41f71b 100644
--- a/col/src/main/java/vct/col/ast/stmt/decl/NameSpace.java
+++ b/col/src/main/java/vct/col/ast/stmt/decl/NameSpace.java
@@ -139,7 +139,6 @@ public NameSpace add(ASTNode item) {
     } else if (item==null) {
     } else {
       hre.lang.System.Warning("cannot insert %s into name space.",item);
-      //Abort("cannot insert %s into name space.",item.getClass());
     }
     return this;
   }
diff --git a/col/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java b/col/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java
index 4ffc94c07b..8bc8123edd 100644
--- a/col/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java
+++ b/col/src/main/java/vct/col/ast/stmt/decl/ProgramUnit.java
@@ -90,22 +90,7 @@ public Iterable<ASTDeclaration> get(){
   private HashMap<ClassName,Method> adt_map=new HashMap<ClassName,Method>();
   
   private HashMap<ClassName,Method> proc_map=new HashMap<ClassName,Method>();
-  
-  /*
-  public void addClass(ClassName name,ASTClass cl){
-    classes.put(name,cl);
-    cl.attach(this,name);
-  }
-  
-  public void addClass(String name[],ASTClass cl){
-    addClass(new ClassName(name),cl);
-  }
 
-  public void addClass(ClassType type,ASTClass cl){
-    addClass(type.getNameFull(),cl);
-  }
-  */
-  
   /**
    * Create an empty program unit.
    */
diff --git a/col/src/main/java/vct/col/ast/syntax/CSyntax.java b/col/src/main/java/vct/col/ast/syntax/CSyntax.java
index b1ba446a46..057273cb4b 100644
--- a/col/src/main/java/vct/col/ast/syntax/CSyntax.java
+++ b/col/src/main/java/vct/col/ast/syntax/CSyntax.java
@@ -80,12 +80,9 @@ public static void setCommon(Syntax syntax){
     
     syntax.addPrimitiveType(PrimitiveSort.Double,"double");
     syntax.addPrimitiveType(PrimitiveSort.Integer,"int");
-    //syntax.addPrimitiveType(Fraction,"frac");
     syntax.addPrimitiveType(PrimitiveSort.Long,"long");
     syntax.addPrimitiveType(PrimitiveSort.Void,"void");
-    //syntax.addPrimitiveType(Resource,"resource");
     syntax.addPrimitiveType(PrimitiveSort.Boolean,"bool");
-    //syntax.addPrimitiveType(Class,"classtype");
     syntax.addPrimitiveType(PrimitiveSort.Char,"char");
     syntax.addPrimitiveType(PrimitiveSort.Float,"float");
     
diff --git a/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java b/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java
index bd3320e845..0583f285df 100644
--- a/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java
+++ b/col/src/main/java/vct/col/ast/syntax/PVLSyntax.java
@@ -38,10 +38,7 @@ public static PVLSyntax get(){
       syntax.addPostfix(PostDecr,"--",140);
       syntax.addOperator(NewArray,-1,"new ","[","]");
       syntax.addOperator(Subscript,145,"","[","]"); // TODO: check if relative order to Select is OK!
-      //syntax.addInfix(SubType,"<:",90);
-      //syntax.addInfix(SuperType,":>",90);
-      syntax.addInfix(Implies,"==>",30);
-      //syntax.addInfix(IFF,"<==>",30);
+        syntax.addInfix(Implies,"==>",30);
       syntax.addLeftFix(Wand,"-*",30);
       syntax.addFunction(Perm,"Perm");
       syntax.addFunction(HistoryPerm,"HPerm");
@@ -51,13 +48,10 @@ public static PVLSyntax get(){
       syntax.addFunction(Empty,"isEmpty");
       syntax.addFunction(RemoveAt, "removeAt");
       syntax.addFunction(SeqPermutation, "permutationOf");
-      //syntax.addFunction(Head,"head");
-      //syntax.addFunction(Tail,"tail");
-      syntax.addFunction(Value,"Value");
+        syntax.addFunction(Value,"Value");
 
       syntax.addFunction(PointsTo,"PointsTo");
       syntax.addFunction(IterationOwner,"\\owner");
-      //syntax.addFunction(ArrayPerm,"ArrayPerm");
       syntax.addFunction(Old,"\\old");
 
       syntax.addFunction(OptionSome, "Some");
@@ -96,33 +90,13 @@ public static PVLSyntax get(){
       syntax.addLeftFix(Plus,"+",110);
       syntax.addLeftFix(Minus,"-",110);
 
-/*
-      // 10 shift   << >> >>>
-      syntax.addInfix(LeftShift,"<<", 100);
-      syntax.addInfix(RightShift,">>", 100);
-      syntax.addInfix(UnsignedRightShift,">>", 100);
-      //  9 relational  < > <= >= instanceof
-       */
-      syntax.addInfix(LT,"<",90);
+        syntax.addInfix(LT,"<",90);
       syntax.addInfix(LTE,"<=",90);
       syntax.addInfix(GT,">",90);
       syntax.addInfix(GTE,">=",90);
-      /*
-      syntax.addInfix(Instance," instanceof ",90);
-      //  8 equality  == !=
-       * */
       syntax.addInfix(EQ,"==",80);
       syntax.addInfix(NEQ,"!=",80);
-      /*
-      //  7 bitwise AND   &
-      syntax.addInfix(BitAnd,"&",70);
-      //  6 bitwise exclusive OR  ^
-      syntax.addInfix(BitXor,"^",60);
-      //  5 bitwise inclusive OR  |
-      syntax.addInfix(BitOr,"|",50);
-      //  4 logical AND   &&
-       */
-      syntax.addLeftFix(And,"&&",40);
+        syntax.addLeftFix(And,"&&",40);
       syntax.addLeftFix(Star,"**",40);
       //  3 logical OR  ||
       syntax.addLeftFix(Or,"||",30);
@@ -135,43 +109,17 @@ public static PVLSyntax get(){
        */
       syntax.addRightFix(Assign,"=",10);
 
-      /*
-      syntax.addRightFix(AddAssign,"+=",10);
-      syntax.addRightFix(SubAssign,"-=",10);
-      syntax.addRightFix(MulAssign,"*= ",10);
-      syntax.addRightFix(DivAssign,"/=",10);
-      syntax.addRightFix(RemAssign,"%=",10);
-      syntax.addRightFix(AndAssign,"&=",10);
-      syntax.addRightFix(XorAssign,"^=",10);
-      syntax.addRightFix(OrAssign,"|=",10);
-      syntax.addRightFix(ShlAssign,"<<=",10);
-      syntax.addRightFix(ShrAssign,">>=",10);
-      syntax.addRightFix(SShrAssign,">>>=",10);
-      
-      syntax.addPrimitiveType(Double,"double");
-      */
-      syntax.addPrimitiveType(PrimitiveSort.Integer,"int");
+        syntax.addPrimitiveType(PrimitiveSort.Integer,"int");
       syntax.addPrimitiveType(PrimitiveSort.ZFraction,"zfrac");
       syntax.addPrimitiveType(PrimitiveSort.Fraction,"frac");
-      //syntax.addPrimitiveType(Long,"long");
       syntax.addPrimitiveType(PrimitiveSort.Void,"void");
       syntax.addPrimitiveType(PrimitiveSort.Resource,"resource");
       syntax.addPrimitiveType(PrimitiveSort.Boolean,"boolean");
       syntax.addPrimitiveType(PrimitiveSort.Process,"process");
       syntax.addPrimitiveType(PrimitiveSort.String,"string");
       syntax.addPrimitiveType(PrimitiveSort.Map,"map");
-      
-      /*
-      syntax.addPrimitiveType(Class,"classtype");
-      syntax.addPrimitiveType(Char,"char");
-      syntax.addPrimitiveType(Float,"float");
-      */
-      //syntax.addPrimitiveType(UInteger,"/*unsigned*/ int");
-      //syntax.addPrimitiveType(ULong,"/*unsigned*/ long");
-      //syntax.addPrimitiveType(UShort,"/*unsigned*/ short");
-      //syntax.addPrimitiveType(Short,"short");
-      
-      syntax.addReserved(FullPerm,"write");
+
+        syntax.addReserved(FullPerm,"write");
       syntax.addReserved(ReadPerm,"read");
       syntax.addReserved(NoPerm,"none");
       syntax.addReserved(EmptyProcess,"empty");
diff --git a/col/src/main/java/vct/col/ast/syntax/Syntax.java b/col/src/main/java/vct/col/ast/syntax/Syntax.java
index 25aa9ee4d3..300712bd51 100644
--- a/col/src/main/java/vct/col/ast/syntax/Syntax.java
+++ b/col/src/main/java/vct/col/ast/syntax/Syntax.java
@@ -256,13 +256,7 @@ public void addReserved(ASTReserved word,String string) {
     syntax2reserved.put(string,word);
   }
 
-/*  
-  public Iterable<String> reserved(){
-    return reserved2syntax.keySet();
-  }
-*/
-  
-  public boolean is_reserved(String text) {
+    public boolean is_reserved(String text) {
     return syntax2reserved.containsKey(text);
   }
 
diff --git a/col/src/main/java/vct/col/ast/type/PrimitiveType.java b/col/src/main/java/vct/col/ast/type/PrimitiveType.java
index b9be137ecf..2dea2dd3fb 100644
--- a/col/src/main/java/vct/col/ast/type/PrimitiveType.java
+++ b/col/src/main/java/vct/col/ast/type/PrimitiveType.java
@@ -189,7 +189,6 @@ public boolean supertypeof(ProgramUnit context, Type t) {
     }
     if (t instanceof PrimitiveType){
       PrimitiveType pt=(PrimitiveType)t;
-      //Warning("testing (%s/%s)",this.sort,pt.sort);
       if (equals(pt)) return true;
       switch(this.sort){
       case Void:
diff --git a/col/src/main/java/vct/col/ast/util/ASTFactory.java b/col/src/main/java/vct/col/ast/util/ASTFactory.java
index afe768e435..336e64271d 100644
--- a/col/src/main/java/vct/col/ast/util/ASTFactory.java
+++ b/col/src/main/java/vct/col/ast/util/ASTFactory.java
@@ -766,7 +766,6 @@ public OperatorExpression new_record(Type type,ASTNode ... args){
    * Create an instantiation of a new object and invoke a constructor on it.
    */
   public MethodInvokation new_object(ClassType type,ASTNode ... args){
-    //return expression(StandardOperator.Build,type,args);
     return invokation(null,type,Method.JavaConstructor, args);
   }
   
diff --git a/col/src/main/java/vct/col/ast/util/ASTFrame.java b/col/src/main/java/vct/col/ast/util/ASTFrame.java
index 5d4a70137d..3252e8d890 100644
--- a/col/src/main/java/vct/col/ast/util/ASTFrame.java
+++ b/col/src/main/java/vct/col/ast/util/ASTFrame.java
@@ -159,27 +159,10 @@ protected ASTNode getAncestor(int stepsBack) {
 
 
   public void enter_before(ASTNode node){
-    /* Might be needed or not:
-    variables.enter();
-    if (node.getParent() instanceof MethodInvokation){
-      MethodInvokation mi=(MethodInvokation)node.getParent();
-      Contract c=null;
-      if (mi.getDefinition()!=null){
-        c=mi.getDefinition().getContract();
-      }
-      if (c!=null){
-        for(DeclarationStatement decl:c.given){
-          variables.add(decl.getName(),new VariableInfo(decl,NameExpressionKind.Argument));
-        }
-        scan_labels(c.pre_condition);
-      }
-    }
-    */
+
   }
   public void leave_before(ASTNode node){
-    /* must match enter! 
-    variables.leave();
-    */
+
   }
   public void enter_after(ASTNode node){
     if (scope!=null) scope.enter_after(node);
@@ -233,18 +216,7 @@ public void visit(AxiomaticDataType adt) {
       }
     }
  
-/*
-    @Override
-    public void visit( node){
-      switch(action){
-      case ENTER:
-        break;
-      case LEAVE:
-        break;
-      }
-    }
-  */
-    
+
     @Override
     public void visit(MethodInvokation node){
       switch(action){
@@ -409,9 +381,6 @@ public void visit(BlockStatement node){
         if (node.getParent() instanceof MethodInvokation){
           MethodInvokation s=(MethodInvokation)node.getParent();
           Method def=s.getDefinition();
-          //if (def==null) {
-          //  Warning("definition of method invokation is unknown, expect type errors.");
-          //}
           add_contract_vars(def);
         }
         BlockStatement block=(BlockStatement)node;
@@ -607,7 +576,6 @@ private void add_contract_vars(Method m) {
 
   
   private void scan_labels(ASTNode node) {
-    //if (node instanceof MethodInvokation){
       for(NameExpression label:node.getLabels()){
         variables.add(label.getName(),new VariableInfo(node, NameExpressionKind.Label));
       }
@@ -618,7 +586,6 @@ private void scan_labels(ASTNode node) {
           variables.add(label.getName(),new VariableInfo(node, NameExpressionKind.Label));
         }
       }
-    //}
     if (node instanceof OperatorExpression){
       for (ASTNode arg : ((OperatorExpression)node).argsJava()) {
         scan_labels(arg);
diff --git a/col/src/main/java/vct/col/ast/util/AbstractRewriter.java b/col/src/main/java/vct/col/ast/util/AbstractRewriter.java
index 6a1e194278..e6d9fbf9df 100644
--- a/col/src/main/java/vct/col/ast/util/AbstractRewriter.java
+++ b/col/src/main/java/vct/col/ast/util/AbstractRewriter.java
@@ -316,7 +316,6 @@ public void visit(AssignmentStatement s) {
 
   @Override
   public void visit(ASTClass c) {
-    //checkPermission(c);
     String name=c.getName();
     if (name==null) {
       Abort("illegal class without name");
@@ -344,7 +343,6 @@ public void visit(ASTClass c) {
 
   @Override
   public void visit(BlockStatement s) {
-    //checkPermission(s);
     Debug("rewriting block");
     BlockStatement tmp=currentBlock;
     currentBlock=new BlockStatement();
@@ -364,7 +362,6 @@ public void visit(BlockStatement s) {
   }
 
   public void visit(ClassType t){
-    //checkPermission(t);
     ClassType res = new ClassType(t.getNameFull(), rewrite(t.argsJava()));
     res.setOrigin(t.getOrigin());
     result=res;
@@ -378,13 +375,11 @@ public void visit(Contract c){
   
   @Override
   public void visit(ConstantExpression e) {
-    //checkPermission(e);
     result=new ConstantExpression(e.value(),e.getType(),e.getOrigin());
   }
   
   @Override
   public void visit(DeclarationStatement s) {
-    //checkPermission(s);
     Type t=s.getType();
     ASTNode tmp=t.apply(this);
     if (tmp instanceof Type){
@@ -420,7 +415,6 @@ public void visit(FunctionType t) {
 
   @Override
   public void visit(IfStatement s) {
-    //checkPermission(s);
     IfStatement res=new IfStatement();
     res.setOrigin(s.getOrigin());
     int N=s.getCount();
@@ -445,7 +439,6 @@ public void visit(ForEachLoop s){
   
   @Override
   public void visit(LoopStatement s) {
-    //checkPermission(s);
     LoopStatement res=new LoopStatement();
     ASTNode tmp;
     tmp=s.getInitBlock();
@@ -467,7 +460,6 @@ public void visit(LoopStatement s) {
 
   @Override
   public void visit(Method m) {
-    //checkPermission(m);
     String name=m.getName();
     if (currentContractBuilder==null) currentContractBuilder=new ContractBuilder();
     DeclarationStatement args[]=rewrite(m.getArgs());
@@ -498,7 +490,6 @@ public void visit(Method m) {
 
   @Override
   public void visit(NameExpression e) {
-    //checkPermission(e);
     NameExpression res=new NameExpression(e.getKind(),e.reserved(),e.getName());
     res.setOrigin(e.getOrigin());
     result=res;
@@ -506,7 +497,6 @@ public void visit(NameExpression e) {
 
   @Override
   public void visit(OperatorExpression e) {
-    //checkPermission(e);
     StandardOperator op=e.operator();
     
     List<ASTNode> args = new LinkedList<ASTNode>();
@@ -516,14 +506,12 @@ public void visit(OperatorExpression e) {
     }
     
     OperatorExpression res = create.expression(op, args);
-    //res.setOrigin(e.getOrigin());
     res.set_before(rewrite(e.get_before()));
     res.set_after(rewrite(e.get_after()));
     result=res;
   }
 
   public void visit(PrimitiveType t){
-    //checkPermission(t);
     PrimitiveType res=new PrimitiveType(t.sort,rewrite(t.argsJava()));
     if (t.getOrigin()!=null){
       res.setOrigin(t);
@@ -534,13 +522,11 @@ public void visit(PrimitiveType t){
   }
 
   public void visit(RecordType t){
-    //checkPermission(t);
     throw new Error("missing case in rewriter: "+t.getClass());
   }
 
   @Override
   public void visit(ReturnStatement s) {
-    //checkPermission(s);
     ASTNode val=s.getExpression();
     if(val!=null) val=val.apply(this);
     ReturnStatement res=new ReturnStatement(val);
@@ -550,7 +536,6 @@ public void visit(ReturnStatement s) {
   }
   @Override
   public void visit(StandardProcedure p) {
-    //checkPermission(p);
     StandardProcedure res = new StandardProcedure(p.operator());
     res.setOrigin(p.getOrigin());
     result=res;
diff --git a/col/src/main/java/vct/col/ast/util/RecursiveVisitor.java b/col/src/main/java/vct/col/ast/util/RecursiveVisitor.java
index 934d113867..a62009ed1d 100644
--- a/col/src/main/java/vct/col/ast/util/RecursiveVisitor.java
+++ b/col/src/main/java/vct/col/ast/util/RecursiveVisitor.java
@@ -230,12 +230,7 @@ public void visit(LoopStatement s) {
 
   @Override
   public void visit(Method m) {
-//    dispatch(m.getContract());
-//    if (c!=null){
-//      dispatch(c.pre_condition);
-//      dispatch(c.post_condition);
-//    }
-    dispatch(m.getReturnType());
+      dispatch(m.getReturnType());
     dispatch(m.getArgs());
     dispatch(m.signals);
     Contract c=m.getContract();
@@ -261,7 +256,6 @@ public void visit(ActionBlock ab){
     dispatch(ab.process());
     dispatch(ab.action());
     // TODO: enable visiting map elements.
-    //dispatch(ab.map().values().to);
     dispatch(ab.block());
   }
   
diff --git a/col/src/main/java/vct/col/ast/util/SequenceUtils.java b/col/src/main/java/vct/col/ast/util/SequenceUtils.java
index 1d6d3e5389..31bf51ffa1 100644
--- a/col/src/main/java/vct/col/ast/util/SequenceUtils.java
+++ b/col/src/main/java/vct/col/ast/util/SequenceUtils.java
@@ -190,35 +190,35 @@ public static ASTNode access(ASTFactory<?> create, ASTNode seq, ASTNode index) {
     }
 
     public static ASTNode accessUsingType(ASTFactory<?> create, Type sequenceType, ASTNode seq, ASTNode index) {
-//        SequenceInfo info = getTypeInfo(sequenceType);
-//        if(info == null) return null;
-//
-//        ASTNode result = seq;
-//
-//        if(info.isOpt()) {
-//            result = create.expression(StandardOperator.OptionGet, result);
-//        }
-//
-//        switch(info.getSequenceSort()) {
-//            case Array:
-//            case Sequence:
-//                result = create.expression(StandardOperator.Subscript, result, index);
-//                break;
-//            default:
-//                throw new UnsupportedOperationException("unimplemented");
-//        }
-//
-//        if(info.isCell()) {
-//            result = create.dereference(result, "item");
-//        }
-//
-//        return result;
-
-        // TODO: Rewrite all sequence access to be specific, as above.
-        // Currently, StandardOperator.Subscript is treated as the generic sequence subscript before the RewriteArrayRef
-        // stage, after which it is rewritten to a specific, correct expression. This should just be the correct
-        // expression from the start. For now, this method assumes we are before the RewriteArrayRef stage. A similar
-        // statement is true for StandardOperator.Size/Length
+         /*SequenceInfo info = getTypeInfo(sequenceType);
+         if(info == null) return null;
+
+         ASTNode result = seq;
+
+         if(info.isOpt()) {
+             result = create.expression(StandardOperator.OptionGet, result);
+         }
+
+         switch(info.getSequenceSort()) {
+             case Array:
+             case Sequence:
+                 result = create.expression(StandardOperator.Subscript, result, index);
+                 break;
+             default:
+                 throw new UnsupportedOperationException("unimplemented");
+         }
+
+         if(info.isCell()) {
+             result = create.dereference(result, "item");
+         }
+
+         return result;*/
+
+          /*TODO: Rewrite all sequence access to be specific, as above.
+          Currently, StandardOperator.Subscript is treated as the generic sequence subscript before the RewriteArrayRef
+          stage, after which it is rewritten to a specific, correct expression. This should just be the correct
+          expression from the start. For now, this method assumes we are before the RewriteArrayRef stage. A similar
+          statement is true for StandardOperator.Size/Length */
 
         return create.expression(StandardOperator.Subscript, seq, index);
     }
diff --git a/hre/src/main/java/hre/ast/FileContext.java b/hre/src/main/java/hre/ast/FileContext.java
index 412a96609b..6783b4ee41 100644
--- a/hre/src/main/java/hre/ast/FileContext.java
+++ b/hre/src/main/java/hre/ast/FileContext.java
@@ -46,7 +46,6 @@ public FileContext(Path filePath, boolean use_gui){
             Debug("Couldn't insert initial text into text pane.");
           }
       }
-      //gui.paneScrollPane.scrollRectToVisible(aRect);
       in.close();
       if (use_gui) SwingUtilities.invokeLater(new Runnable() {
         public void run() {
@@ -153,16 +152,4 @@ public void mark(FileOrigin o, String result) {
     }
   }
   
-  /* Code related to scrolling to a given location..
-      Rectangle s=gui.textPane.getBounds();
-      Rectangle r=gui.textPane.getVisibleRect();
-      Rectangle p=null;
-      try {
-        p = gui.textPane.modelToView(4000);
-        gui.textPane.scrollRectToVisible(p);
-      } catch (BadLocationException e) {
-        // TODO Auto-generated catch block
-      }
-   */
-
 }
diff --git a/hre/src/main/java/hre/ast/TrackingOutput.java b/hre/src/main/java/hre/ast/TrackingOutput.java
index 40a9a1a78c..06134deaee 100644
--- a/hre/src/main/java/hre/ast/TrackingOutput.java
+++ b/hre/src/main/java/hre/ast/TrackingOutput.java
@@ -13,7 +13,6 @@
  */
 public class TrackingOutput {
   private PrintWriter output;
-//  private boolean show;
 
   private static class Frame {
     public int line,col;
diff --git a/parsers/src/main/java/vct/parsers/rewrite/KernelBodyRewriter.java b/parsers/src/main/java/vct/parsers/rewrite/KernelBodyRewriter.java
index 83c8f75fce..03ba277acd 100644
--- a/parsers/src/main/java/vct/parsers/rewrite/KernelBodyRewriter.java
+++ b/parsers/src/main/java/vct/parsers/rewrite/KernelBodyRewriter.java
@@ -122,11 +122,6 @@ public void visit(Method m) {
         kcb.given(rewrite(c.given));
         kcb.yields(rewrite(c.yields));
         BlockStatement body = (BlockStatement) rewrite(m.getBody());
-        //body.prepend(create.field_decl("opencl_tid",create.primitive_type(Sort.Integer),
-        //    plus(mult(create.local_name("opencl_gid"),create.local_name("opencl_gsize")),create.local_name("opencl_lid"))));
-        //icb.given(create.field_decl("opencl_tid",create.primitive_type(Sort.Integer)));
-        //icb.requires(create.expression(StandardOperator.EQ,
-        //    create.local_name("opencl_tid"),plus(mult(create.local_name("opencl_gid"),create.local_name("opencl_gsize")),create.local_name("opencl_lid"))));
         DeclarationStatement[] iters = new DeclarationStatement[]{inner_decl};
         body = create.block(create.region(null, create.parallel_block("group_block", icb.getContract(), iters, body)));
         iters = new DeclarationStatement[]{outer_decl};
diff --git a/src/main/java/vct/col/rewrite/AccessIntroduce.java b/src/main/java/vct/col/rewrite/AccessIntroduce.java
index d7397d6971..f8e222d50d 100644
--- a/src/main/java/vct/col/rewrite/AccessIntroduce.java
+++ b/src/main/java/vct/col/rewrite/AccessIntroduce.java
@@ -33,7 +33,6 @@ public void visit(OperatorExpression e){
     }
     case Subscript:{
       super.visit(e);
-      //result=create.expression(StandardOperator.Get,result);
       break;
     }
     default:
diff --git a/src/main/java/vct/col/rewrite/AddSimpleTriggers.java b/src/main/java/vct/col/rewrite/AddSimpleTriggers.java
index b252ff4b52..e91bee884a 100644
--- a/src/main/java/vct/col/rewrite/AddSimpleTriggers.java
+++ b/src/main/java/vct/col/rewrite/AddSimpleTriggers.java
@@ -47,7 +47,6 @@ private ASTNode[][] getTriggers(DeclarationStatement[] declarations, ASTNode mai
     ASTNode[] nodes = res.toArray(new ASTNode[res.size()]);
     HashSet<HashSet<ASTNode>> sets = powerSet(0, nodes);
     sets = validSets(sets, declarations);
-    // sets = minimumSets(sets, nodes);
     for (HashSet<ASTNode> set : sets) {
       triggerSets.add(set.toArray(new ASTNode[set.size()]));
     }
diff --git a/src/main/java/vct/col/rewrite/CSLencoder.java b/src/main/java/vct/col/rewrite/CSLencoder.java
index 4e422adc5c..a1acef21de 100644
--- a/src/main/java/vct/col/rewrite/CSLencoder.java
+++ b/src/main/java/vct/col/rewrite/CSLencoder.java
@@ -51,29 +51,6 @@ private boolean has_csl_inv(ASTClass cl){
   
   @Override
   public void visit(Method m){
-    /*
-    if(m.kind==Method.Kind.Constructor && has_csl_inv((ASTClass)m.getParent())){
-      Method.Kind kind=Method.Kind.Constructor;
-      ContractBuilder cb=new ContractBuilder();
-      rewrite(m.getContract(),cb);
-      cb.ensures(create.invokation(create.diz(),null,"csl_invariant"));
-      String name = m.name();
-      DeclarationStatement args[]=rewrite(m.getArgs());
-      BlockStatement body;
-      if (m.getBody()!=null){
-        body=(BlockStatement)rewrite(m.getBody());
-        body.addStatement(create.special(ASTSpecial.Kind.Fold,
-            create.invokation(create.diz(),null,"csl_invariant")
-        ));   
-      } else {
-        body=null;
-      }
-      Contract contract=cb.getContract();
-      Type returns=rewrite(m.getReturnType());
-      result=create.method_kind(kind, returns, contract, name, args, m.usesVarArgs(), body);
-    } else {
-      super.visit(m);
-    }*/
     // TODO PB: disabling this is unsound, but this logic cannot be combined with JavaEncoder: it was already disabled accidentally.
     super.visit(m);
   }
diff --git a/src/main/java/vct/col/rewrite/DynamicStaticInheritance.java b/src/main/java/vct/col/rewrite/DynamicStaticInheritance.java
index 242452a8bc..b041618e3a 100644
--- a/src/main/java/vct/col/rewrite/DynamicStaticInheritance.java
+++ b/src/main/java/vct/col/rewrite/DynamicStaticInheritance.java
@@ -66,7 +66,6 @@ public static boolean isSuper(ASTNode n){
 
   private AbstractRewriter tag_this=new AbstractRewriter(this){
     public void visit(MethodInvokation e){
-//      if (isThis(e.object())&&(e.getDefinition()==null||e.getDefinition().getKind()==Method.Kind.Predicate)){
       if (isThis(e.object())){
         String class_name=this.current_class().getName();
         result=create.invokation(rewrite(e.object()), rewrite(e.dispatch()), e.method()+AT_STRING+class_name, rewrite(e.getArgs()));
@@ -242,7 +241,6 @@ public void visit(ASTClass cl){
     String class_name=cl.getName();
     ASTClass res=create.ast_class(class_name,cl.kind,rewrite(cl.parameters),new ClassType[0],new ClassType[0]);
     //should be function, but chalice messes up during printing.
-    //res.add_dynamic(create.method_kind(Method.Kind.Pure,create.primitive_type(Sort.Boolean),null,"is_a_"+class_name,new DeclarationStatement[0],null));
     res.add_dynamic(create.predicate("is_a_"+class_name, null));
     res.add_dynamic(create.predicate("instance_of_"+class_name, null));
     for(DeclarationStatement decl:cl.fields()){
@@ -311,20 +309,6 @@ public void visit(ASTClass cl){
         open.setStatic(m.isStatic());
         res.add(open);
         ASTNode body=tag_this.rewrite(m.getBody());
-        /* DELETE due to override instead of chain...
-        if (parent!=null){
-          for(int i=0;i<N;i++){
-            names[i]=create.local_name(m.getArgument(i));
-          }
-          ASTNode base=create.invokation(
-              create.reserved_name(This),
-              null,
-              m.getName()+AT_STRING+parent.getName(),
-              names);
-          base.labeled("parent");
-          body=create.expression(StandardOperator.Star,base,body);
-        }
-        */
         Method local=create.method_kind(
             m.kind,
             copy_rw.rewrite(m.getReturnType()),
diff --git a/src/main/java/vct/col/rewrite/FlattenBeforeAfter.java b/src/main/java/vct/col/rewrite/FlattenBeforeAfter.java
index c6b1c6dbd1..f7574537cb 100644
--- a/src/main/java/vct/col/rewrite/FlattenBeforeAfter.java
+++ b/src/main/java/vct/col/rewrite/FlattenBeforeAfter.java
@@ -20,7 +20,6 @@ public void visit(BlockStatement s){
     for(ASTNode item:s){
       ASTNode tmp=rewrite(item);
       if ((tmp instanceof BeforeAfterAnnotations) && !(tmp instanceof MethodInvokation)){
-        //Warning("moving %s",tmp.getClass());
         BeforeAfterAnnotations baa=(BeforeAfterAnnotations) tmp;
         BlockStatement before=baa.get_before();
         BlockStatement after=baa.get_after();
@@ -37,11 +36,7 @@ public void visit(BlockStatement s){
           res.add(n);
         }
       } else {
-        //if (tmp instanceof ASTSpecial){
-        //  Warning("skipping %s containsing %s",((ASTSpecial)tmp).kind,((ASTSpecial)tmp).args[0].getClass());
-        //}
-        //Warning("skipping %s",tmp.getClass());
-        res.add(tmp);
+          res.add(tmp);
       }
     }
     result=res;
diff --git a/src/main/java/vct/col/rewrite/GhostLifter.java b/src/main/java/vct/col/rewrite/GhostLifter.java
index c153d05db5..5ad77e6184 100644
--- a/src/main/java/vct/col/rewrite/GhostLifter.java
+++ b/src/main/java/vct/col/rewrite/GhostLifter.java
@@ -81,13 +81,11 @@ public void visit(MethodInvokation m){
         if (s.location() instanceof NameExpression){
           NameExpression name=(NameExpression)s.location();
           //TODO: make kind checking work
-          //if (name.getKind()==NameExpressionKind.Label){
             if (arg_map.containsKey(name.getName())){
               Fail("%s is assigned twice",name.getName());
             }
             arg_map.put(name.getName(), rewrite(s.expression()));
             continue;
-          //}
         }
       }
       before.add(rewrite(n));
@@ -98,13 +96,11 @@ public void visit(MethodInvokation m){
         if (s.expression() instanceof NameExpression){
           NameExpression name=(NameExpression)s.expression();
           //TODO: make kind checking work
-          //if (name.getKind()==NameExpressionKind.Label){
             if (arg_map.containsKey(name.getName())){
               Fail("%s is assigned twice",name.getName());
             }
             arg_map.put(name.getName(), rewrite(s.location()));
             continue;
-          //}
         }
       }
       after.add(rewrite(n));
diff --git a/src/main/java/vct/col/rewrite/GlobalizeStatics.java b/src/main/java/vct/col/rewrite/GlobalizeStatics.java
index 1445bb2cac..1654b72dde 100644
--- a/src/main/java/vct/col/rewrite/GlobalizeStatics.java
+++ b/src/main/java/vct/col/rewrite/GlobalizeStatics.java
@@ -107,23 +107,6 @@ public void visit(StructValue v){
     if (v.type() instanceof ClassType){
       Abort("illegal use of struct value for constructor call");
     }
-    /*
-    switch(e.getOperator()){
-    case Build:{
-      if (e.getArg(0) instanceof ClassType){
-        // Constructor call encoded as Build.
-        ASTNode args[]=rewrite(null,e.getArguments());
-        args[0]=args[1];
-        if (processing_static){
-          args[1]=create.reserved_name(ASTReserved.This);
-        } else {
-          args[1]=create.local_name("global");
-        }
-        result=create.expression(StandardOperator.Build, args);
-        return;
-      }
-    }
-    }*/
     super.visit(v);
   }
   
diff --git a/src/main/java/vct/col/rewrite/KernelRewriter.java b/src/main/java/vct/col/rewrite/KernelRewriter.java
index 72bdb76732..3cc000c31d 100644
--- a/src/main/java/vct/col/rewrite/KernelRewriter.java
+++ b/src/main/java/vct/col/rewrite/KernelRewriter.java
@@ -134,11 +134,6 @@ public void visit(ParallelBarrier pb){
     if (Configuration.auto_barrier.get()){
       currentBlock.add(create_barrier_call(no.intValue()));
       //Disabled these hints because old in barrier refers to before barrier... 
-      //for(ASTNode clause : ASTUtils.conjuncts(pb.contract.post_condition,StandardOperator.Star)){
-      //  if (clause.getType().isBoolean()){
-      //    currentBlock.add(create.expression(StandardOperator.Assert, rewrite(clause)));
-      //  }
-      //}
     } else {
       Stack<ASTNode> resource_stack=new Stack<ASTNode>();
       // check and keep resources.
@@ -572,7 +567,6 @@ public void visit(ASTClass cl){
               ));
             }
           }
-          //cb.requires(create.fold(StandardOperator.Star, barrier_pre.get(i)));
           if (barrier_pre.get(i)!=null) for(ASTNode claim:barrier_pre.get(i)){
               if (!claim.getType().isBoolean()){
                 if (Configuration.auto_barrier.get()){
@@ -628,7 +622,6 @@ public void visit(ASTClass cl){
 
   @Override
   public void visit(LoopStatement s) {
-    //checkPermission(s);
     LoopStatement res=new LoopStatement();
     ASTNode tmp;
     tmp=s.getInitBlock();
@@ -647,7 +640,6 @@ public void visit(LoopStatement s) {
       Set<Integer> preds=new HashSet<Integer>();
       find_predecessors(preds,s.getBody());
       for(Integer i : preds){
-        //Warning("    %d",i);
         inv1=create.expression(StandardOperator.Or,inv1,
               create.expression(StandardOperator.EQ,
                   create.local_name("__last_barrier"),
diff --git a/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java b/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
index 9edb9c7eb8..aee97374d5 100644
--- a/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
+++ b/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
@@ -63,84 +63,19 @@ public void visit(ParallelBlock pb){
       Fail("parallel block without a contract");
     }
     blocks.push(pb);
-    
-    /*
-    count++;
-    String main_name="parallel_block_main_"+count;
-    String check_name="parallel_block_check_"+count;
-    String local_suffix="_local_"+count;
-    Hashtable<String,Type> main_vars=free_vars(pb);
-    Debug("free main vars: %s",main_vars);
-    Hashtable<String,Type> check_vars=new Hashtable(main_vars);
-    ContractBuilder main_cb=new ContractBuilder();
-    ContractBuilder check_cb=new ContractBuilder();
-    Hashtable<NameExpression,ASTNode> map=new Hashtable();
-    Substitution sigma=new Substitution(source(),map);
-    */
+
     DeclarationStatement iters[] = pb.itersJava().toArray(new DeclarationStatement[0]);
     DeclarationStatement iter_decls[] = new DeclarationStatement[iters.length];
-    //iter_decls_prime = new DeclarationStatement[pb.iters.length];
     ArrayList<ASTNode> guard_list=new ArrayList<ASTNode>();
-    /*
-    ArrayList<ASTNode> guard_prime_list_before=new ArrayList();
-    ArrayList<ASTNode> guard_prime_list_after=new ArrayList();
-    Hashtable<NameExpression,ASTNode> prime=new Hashtable();
-    */
     for (int i = 0; i < iter_decls.length; i++) {
       iter_decls[i] = create.field_decl(iters[i].name(), iters[i].getType());
-      //iter_decls_prime[i]=create.field_decl(pb.iters[i].name+"__prime", pb.iters[i].getType());
       ASTNode member = create.local_name(iters[i].name());
       member.setType(iters[i].getType());
       ASTNode tmp = create.expression(StandardOperator.Member, member, iters[i].initJava());
       guard_list.add(tmp);
-      /*
-      check_cb.requires(tmp);
-      check_cb.ensures(tmp);
-      OperatorExpression range=(OperatorExpression)pb.iters[i].getInit();
-      tmp=create.expression(StandardOperator.RangeSeq,range.getArg(0),create.unresolved_name(pb.iters[i].name));
-      tmp=create.expression(StandardOperator.Member,create.unresolved_name(pb.iters[i].name+"__prime"),tmp);
-      guard_prime_list_before.add(tmp);
-      tmp=create.expression(StandardOperator.Plus,create.unresolved_name(pb.iters[i].name),create.constant(1));
-      tmp=create.expression(StandardOperator.RangeSeq,tmp,range.getArg(1));
-      tmp=create.expression(StandardOperator.Member,create.unresolved_name(pb.iters[i].name+"__prime"),tmp);
-      guard_prime_list_after.add(tmp);
-      check_vars.put(pb.iters[i].name,pb.iters[i].getType());
-      prime.put(create.local_name(pb.iters[i].name),create.local_name(pb.iters[i].name+"__prime"));
-      */
     }
     ASTNode iters_guard=create.fold(StandardOperator.And,guard_list);
-    /*
-    sigma_prime=new Substitution(source(),prime);
-    iters_guard_prime_before=create.fold(StandardOperator.And,guard_prime_list_before);
-    iters_guard_prime_after=create.fold(StandardOperator.And,guard_prime_list_after);
-    
-    for(ASTNode clause:ASTUtils.conjuncts(c.pre_condition, StandardOperator.Star)){
-      check_cb.requires(clause);
-      if (clause.getType().isBoolean()){
-        main_cb.requires(create.forall(copy_rw.rewrite(iters_guard), rewrite(clause) , iter_decls));
-      } else {
-        main_cb.requires(create.starall(copy_rw.rewrite(iters_guard), rewrite(clause) , iter_decls));
-      }
-    }
-    
-    for(ASTNode clause:ASTUtils.conjuncts(c.post_condition, StandardOperator.Star)){
-      check_cb.ensures(clause);
-      if (clause.getType().isBoolean()){
-        main_cb.ensures(create.forall(copy_rw.rewrite(iters_guard), rewrite(clause) , iter_decls));
-      } else {
-        main_cb.ensures(create.starall(copy_rw.rewrite(iters_guard), rewrite(clause) , iter_decls));
-      }
-    }
-    currentTargetClass.add(create.final_method_decl()(
-        create.primitive_type(Sort.Void),
-        check_cb.getContract(),
-        check_name,
-        gen_pars(check_vars),
-        rewrite(pb.block)
-    ));
-    Contract res=main_cb.getContract();
-    */
-    
+
     ASTNode res=do_block(new ForEachLoop(iter_decls, iters_guard, pb.block()).setContract(pb.contract()), true);
     
     blocks.pop();
@@ -697,10 +632,8 @@ private ASTNode do_block(ForEachLoop s,final boolean contract){
     for(ASTNode parBound : parBoundsStack)
       parBound.accept(bodyVarScanner);
     Map<String, Type> bodyVars = bodyVarScanner.freeNamesJava();
-    //Hashtable<String,Type> iters=new Hashtable<String,Type>();
     Map<String, Type> mainVars = new HashMap<>(bodyVars);
     for(DeclarationStatement decl:s.decls){
-      //iters.put(decl.name,decl.getType());
       mainVars.remove(decl.name());
     }
 
@@ -957,9 +890,6 @@ protected void check_send_recv(DeclarationStatement[] body_decl, String var_name
 
         cb.requires(create.fold(StandardOperator.And, parBoundsStack));
         // lower bound is already guaranteed by guard check.
-        //cb.requires(create.expression(StandardOperator.LTE,
-        //    create.constant(dr),create.argument_name(var_name)
-        //));
         for(ASTNode g:send_entry.guards){
           cb.requires(shift.rewrite(g));
         }
diff --git a/src/main/java/vct/col/rewrite/RewriteSystem.java b/src/main/java/vct/col/rewrite/RewriteSystem.java
index b0976436ae..1fc44b4e2e 100644
--- a/src/main/java/vct/col/rewrite/RewriteSystem.java
+++ b/src/main/java/vct/col/rewrite/RewriteSystem.java
@@ -119,7 +119,6 @@ public Boolean map(NameExpression e, ASTNode a) {
         return a.isName(dref.name());
       }
       return ref.get().match(a);
-      //throw new HREError("non-linear left-hand side");
     }
   }
 
@@ -616,7 +615,6 @@ public void post_visit(ASTNode node){
       if(d instanceof DeclarationStatement){
         DeclarationStatement decl=(DeclarationStatement)d;
         String name = decl.name();
-        //Warning("variable %s",name);
         vars.add(name);
       }
     }
@@ -626,7 +624,6 @@ public void post_visit(ASTNode node){
       }
       if (d instanceof Axiom){
         Axiom axiom=(Axiom)d;
-        //Warning("axiom %s",axiom.name);
         if (!axiom.rule().isa(StandardOperator.EQ)){
           Fail("not a == rule");
         }
diff --git a/src/main/java/vct/col/rewrite/SilverClassReduction.java b/src/main/java/vct/col/rewrite/SilverClassReduction.java
index 510b12ed71..d36ec6e0e9 100644
--- a/src/main/java/vct/col/rewrite/SilverClassReduction.java
+++ b/src/main/java/vct/col/rewrite/SilverClassReduction.java
@@ -440,9 +440,7 @@ public void visit(OperatorExpression e){
       ClassType t=(ClassType)e.arg(0);
       ASTClass cl=source().find(t);
       ArrayList<ASTNode>args=new ArrayList<ASTNode>();
-      //NameExpression f=create.field_name("A__x");
-      //f.setSite(ref_class);
-      for(DeclarationStatement field:cl.dynamicFields()){
+        for(DeclarationStatement field:cl.dynamicFields()){
         args.add(create.dereference(create.class_type("Ref"), cl.name() + "_" + field.name()));
       }
       result=create.expression(StandardOperator.NewSilver,args.toArray(new ASTNode[0]));
@@ -464,7 +462,6 @@ public void visit(OperatorExpression e){
       } else {
         ASTNode condition=create.invokation(null, null, "instanceof_TYPE_TYPE",
             create.domain_call("TYPE","type_of",object),
-            //create.invokation(null,null,"type_of",object));
             create.domain_call("TYPE","class_"+t));
 
         /* PB: this is incorrect, but dereference(_, ILLEGAL_CAST) is also incorrect... */
diff --git a/src/main/java/vct/col/rewrite/VectorEncode.java b/src/main/java/vct/col/rewrite/VectorEncode.java
index b85a63a813..1260ae1aa4 100644
--- a/src/main/java/vct/col/rewrite/VectorEncode.java
+++ b/src/main/java/vct/col/rewrite/VectorEncode.java
@@ -57,14 +57,8 @@ private static String name(Pair<Op, Type> p){
   
   private HashSet<Pair<Op,Type>> ops=new HashSet<>();
   private HashMap<String, Type> locals;
-  
-  //static ProgramUnit vector_lib;
-  //static {
-  //  File file=new File(new File(Configuration.getHome().toFile(),"config"),"vectorlib.pvl");
-  //  vector_lib=Parsers.getParser("pvl").parse(file);
-  //}
 
-  public VectorEncode(ProgramUnit source) {
+    public VectorEncode(ProgramUnit source) {
     super(source);
   }
   
diff --git a/src/main/java/vct/col/util/AbstractTypeCheck.java b/src/main/java/vct/col/util/AbstractTypeCheck.java
index 27faeac16a..f03af1cdd2 100644
--- a/src/main/java/vct/col/util/AbstractTypeCheck.java
+++ b/src/main/java/vct/col/util/AbstractTypeCheck.java
@@ -217,18 +217,6 @@ public Method find_method(MethodInvokation e){
       Objects.requireNonNull(cl, () -> String.format("could not find class %s used in %s", object_type.getFullName(), e));
       m=cl.find(e.method(), object_type, type, JavaASTClassLoader.INSTANCE(), currentNamespace);
       if (m==null) {
-        /*
-        String parts[]=e.method.split("_");
-        if (parts.length==3 && parts[1].equals("get")){
-          // TODO: check if parts[0] is a predicate.
-          DeclarationStatement field=cl.find_field(parts[2]);
-          if (field!=null) {
-            Warning("assuming %s is implicit getter function",e.method);
-            e.setType(field.getType());
-          }
-          return;
-        }
-        */
         String tmp="";
         if (N>0){
           tmp=type[0].toString();
@@ -330,115 +318,6 @@ public void visit(MethodInvokation e){
       }
     }
 
-    /*
-    //m=source().find_procedure(e.method);
-    if (m!=null){
-      e.setDefinition(m);
-      Type t=m.getReturnType();
-      e.setType(t);
-      int N=m.getArity();
-      if (e.getArity()!=N){
-        Fail("different number of arguments for %s (%d instead of %d)",m.name,e.getArity(),N);
-      }
-      for(int i=0;i<N;i++){
-        Type ti=m.getArgType(i);
-        ASTNode arg=e.getArg(i);
-        if (!ti.supertypeof(source(), arg.getType())){
-          Fail("argument type %d incompatible",i);
-        }
-        if (ti.isPrimitive(PrimitiveType.Sort.Fraction)||
-            ti.isPrimitive(PrimitiveType.Sort.ZFraction)){
-          force_frac(arg);
-        }
-      }
-      return;
-    }
-
-    if (e.object==null){
-      if (e.dispatch!=null){
-        // This is a constructor invokation.
-        ClassType t=e.dispatch;
-        ASTClass cl=source().find(t.getNameFull());
-        if (cl==null){
-          Fail("class %s not found",t);
-        }
-        ASTNode args[]=e.getArgs();
-        Type c_args[]=new Type[args.length];
-        for(int i=0;i<args.length;i++){
-          c_args[i]=args[i].getType();
-          if(c_args[i]==null){
-            Fail("argument %d is not typed",i);
-          }
-        }
-        m=cl.get_constructor(source(),c_args);
-        if(m==null){
-          Fail("Could not find constructor");
-        }
-        e.setType(t);
-        e.setDefinition(m);
-        if (e.get_before()!=null) {
-          enter_before(e);
-          e.get_before().accept(this);
-          leave_before(e);
-        }
-        if (e.get_after()!=null) {
-          enter_after(e);
-          e.get_after().accept(this);
-          leave_after(e);
-        }
-        return;
-      }
-      Abort("unresolved method invokation (%s) at "+e.getOrigin(),e.method);
-    }
-    if (e.object.getType()==null) Abort("object has no type at %s",e.object.getOrigin());
-    if (!(e.object.getType() instanceof ClassType)) Abort("invokation on non-class");
-    ClassType object_type=(ClassType)e.object.getType();
-    int N=e.getArity();
-    for(int i=0;i<N;i++){
-      if (e.getArg(i).labels()>0) {
-        for(int j=i+1;j<N;j++){
-          if (e.getArg(j).labels()==0) Fail("positional argument following named argument");
-        }
-        N=i;
-        break;
-      }
-    }
-    Type type[]=new Type[N];
-    for(int i=0;i<N;i++){
-      type[i]=e.getArg(i).getType();
-      if (type[i]==null) Abort("argument %d has no type.",i);
-    }
-    ASTClass cl=source().find(object_type.getNameFull());
-    if (cl==null) Fail("could not find class %s",object_type.getFullName());
-    m=cl.find(e.method,object_type,type);
-    while(m==null && cl.super_classes.length>0){
-      cl=source().find(cl.super_classes[0].getNameFull());
-      m=cl.find(e.method,object_type,type);
-    }
-    if (m==null){
-      m=source().find_adt(e.method);
-    }
-    if (m==null) {
-      String parts[]=e.method.split("_");
-      if (parts.length==3 && parts[1].equals("get")){
-        // TODO: check if parts[0] is a predicate.
-        DeclarationStatement field=cl.find_field(parts[2]);
-        if (field!=null) {
-          Warning("assuming %s is implicit getter function",e.method);
-          e.setType(field.getType());
-        }
-        return;
-      }
-      String tmp="";
-      if (N>0){
-        tmp=type[0].toString();
-        for(int i=1;i<N;i++){
-          tmp=tmp+","+type[i].toString();
-        }
-      }
-      Fail("could not find method %s(%s) in class %s at %s",e.method,tmp,object_type.getFullName(),e.getOrigin());
-    }
-        */
     switch(m.kind){
     case Constructor:
       if (e.dispatch()!=null){
@@ -1176,9 +1055,6 @@ public void visit(OperatorExpression e) {
         break;
       case Values: {
         Type t = e.arg(0).getType();
-//      if (!t.isPrimitive(PrimitiveSort.Array)){
-//
-//      }
         if (t.isPrimitive(PrimitiveSort.Option)) {
           t = (Type) t.firstarg();
         }
@@ -1214,10 +1090,8 @@ public void visit(OperatorExpression e) {
         }
 
         if (tt[1].supertypeof(source(), tt[0])) {
-          //Warning("ITE type %s",tt[1]);
           e.setType(tt[1]);
         } else if (tt[0].supertypeof(source(), tt[1])) {
-          //Warning("ITE type %s",tt[0]);
           e.setType(tt[0]);
         }
         if (tt[0].isPrimitive(PrimitiveSort.ZFraction) || tt[0].isPrimitive(PrimitiveSort.Fraction)) {
@@ -1773,37 +1647,6 @@ public void visit(StructValue v){
         }
       }
     }
-//    if (v.type()==null){
-//      Abort("Build without type argument");
-//    }
-//    Type t=v.type();
-//    v.setType(t);
-//    if (t instanceof ClassType && !((ClassType) t).getFullName().equals("VCTArray")){
-//      Abort("constructor encoded as struct value");
-//    } else {
-//      if (t.hasArguments()){
-//        Fail("type without arguments: %s in %s",t,v);
-//      }
-//      t=(Type)t.firstarg();
-//
-//      if(t.isPrimitive(PrimitiveSort.Cell)) {
-//        t = (Type) t.firstarg();
-//      }
-//
-//      for (int i = 0; i < v.valuesLength(); i++) {
-//        Type tt[1]=v.value(i).getType();
-//        if (tt[1]==null){
-//          Fail("untyped build argument %d",i);
-//        }
-//        if(t.equals(tt[1]) || t.supertypeof(source(), tt[1]) || (t instanceof ClassType && ((ClassType) t).getFullName().equals("Ref"))) {
-//          if(t.isPrimitive(PrimitiveSort.Option)) {
-//            v.value(i).setType(t);
-//          }
-//        } else {
-//          Abort("cannot use %s to initialize %s", tt[1], t);
-//        }
-//      }
-//    }
   }
 
   private void check_location(ASTNode arg,String what) {
@@ -2008,7 +1851,6 @@ public void visit(LoopStatement s) {
   @Override
   public void visit(BindingExpression e){
     super.visit(e);
-    //result=create.binder(e.binder, rewrite(e.getDeclarations()), rewrite(e.select), rewrite(e.main));
     Type t;
     if (e.select()!=null){
       t=e.select().getType();
diff --git a/src/main/java/vct/silver/SilverBackend.java b/src/main/java/vct/silver/SilverBackend.java
index 15da5341d0..a7e13cc77e 100644
--- a/src/main/java/vct/silver/SilverBackend.java
+++ b/src/main/java/vct/silver/SilverBackend.java
@@ -88,9 +88,9 @@ public static <Program> PassReport TestSilicon(PassReport given, String tool, Vi
     }
 
     Properties settings=new Properties();
-    if (tool.startsWith("silicon")){
-      //settings.setProperty("smt.soft_timeout",silicon_z3_timeout.get()+"");
-    }
+    /*if (tool.startsWith("silicon")){
+      settings.setProperty("smt.soft_timeout",silicon_z3_timeout.get()+"");
+    }*/
     ViperControl control=new ViperControl(log);
     try {
       // Call into Viper to verify!
diff --git a/src/main/java/vct/silver/ViperControl.java b/src/main/java/vct/silver/ViperControl.java
index 6ed6eeb518..cec6cccba7 100644
--- a/src/main/java/vct/silver/ViperControl.java
+++ b/src/main/java/vct/silver/ViperControl.java
@@ -39,7 +39,6 @@ public void run(){
         old_origin=current_origin;
         count=0;
       }
-      //future.cancel(false);
     }
   };
 
@@ -115,7 +114,6 @@ public void progress(String fmt, Object... args) {
   @Override
   public void profile(Origin o,String task){
     if (Configuration.profiling_option.used()){
-      //hre.System.Progress("verifying %s at %s",task,o);
       current_origin=o;
       current_task=task;
     }
diff --git a/viper/src/main/java/viper/api/SilverExpressionMap.java b/viper/src/main/java/viper/api/SilverExpressionMap.java
index 497c1a5f67..6404b29bcd 100644
--- a/viper/src/main/java/viper/api/SilverExpressionMap.java
+++ b/viper/src/main/java/viper/api/SilverExpressionMap.java
@@ -124,9 +124,6 @@ public E map(OperatorExpression e) {
         if (e.arg(1).getType().isBoolean()) {
           return create.and(o, e1, e2);
         }
-//        } else if (e.arg(1).getType().isPrimitive(PrimitiveSort.Byte)) {
-//          break;
-//        }
         // fall through
       }
 
@@ -134,9 +131,6 @@ public E map(OperatorExpression e) {
         if (e.arg(1).getType().isBoolean()) {
           return create.neq(o, e1, e2);
         }
-//        } else if (e.arg(1).getType().isPrimitive(PrimitiveSort.Byte)) {
-//          break;
-//        }
         // fall through
       }
 
@@ -144,9 +138,6 @@ public E map(OperatorExpression e) {
         if (e.arg(1).getType().isBoolean()) {
           return create.or(o, e1, e2);
         }
-//        } else if (e.arg(1).getType().isPrimitive(PrimitiveSort.Byte)) {
-//
-//        }
         // fall through
       }
       case Size:
diff --git a/viper/src/main/java/viper/api/SilverStatementMap.java b/viper/src/main/java/viper/api/SilverStatementMap.java
index 0621d50a77..232788f755 100644
--- a/viper/src/main/java/viper/api/SilverStatementMap.java
+++ b/viper/src/main/java/viper/api/SilverStatementMap.java
@@ -288,7 +288,6 @@ public S map(ASTSpecial special) {
     case Unfold: return create.unfold(special.getOrigin(),special.args[0].apply(expr));
     case Fresh:
       throw new HREError("Fresh is no longer supported in viper. See https://github.com/utwente-fmt/vercors/issues/383");
-      // Old implementation: return create.fresh(special.getOrigin(),do_names(special.args));
     default:
       throw new HREError("cannot map special %s",special.kind);
     }
@@ -409,7 +408,6 @@ private <F extends ASTNode> ArrayList<E> do_names(F args[]){
   @Override
   public S map(Constraining c) {
     throw new HREError("Constraining is no longer supported in viper. See https://github.com/utwente-fmt/vercors/issues/383");
-    // Old implementation: return create.constraining(c.getOrigin(), do_names(c.varsJava()), c.block().apply(this));
   }
 
   @Override
diff --git a/viper/src/main/java/viper/api/VerCorsTypeFactory.java b/viper/src/main/java/viper/api/VerCorsTypeFactory.java
index 525a20617e..e18f864101 100644
--- a/viper/src/main/java/viper/api/VerCorsTypeFactory.java
+++ b/viper/src/main/java/viper/api/VerCorsTypeFactory.java
@@ -55,17 +55,13 @@ public Type Perm() {
   
   @Override
   public Type Ref() {
-    //enter(null);
     Type res=create.class_type("Ref");
-    //leave();
     return res;
   }
 
   @Override
   public Type Set(Type t) {
-    //enter(null);
     Type res=create.primitive_type(PrimitiveSort.Set,t);
-    //leave();
     return res;
   }