From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 19 Mar 2014 14:03:18 +0000 (-0500)
Subject: Fix a memory leak in LFSC proof checker.  Largest QF_UF proof from Morgan (problemati... 
X-Git-Tag: cvc5-1.0.0~7013
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d645cc84b733042833d6617e5ccfac214e62a75;p=cvc5.git

Fix a memory leak in LFSC proof checker.  Largest QF_UF proof from Morgan (problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory.  Add example test proof.
---

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 8ef114115..b550c58a1 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -101,7 +101,7 @@ void eat_rparen() {
 }
 
 void eat_excess(int prev) {
-  while(open_parens > prev) 
+  while(open_parens > prev)
     eat_rparen();
 }
 
@@ -110,8 +110,8 @@ void eat_excess(int prev) {
 1. expected=0, create is false: check() sets computed to be the classifier of
    the checked term.
 
-2. expected=0, create is true: check() returns 
-   the checked expression and sets computed to be its classifier. 
+2. expected=0, create is true: check() returns
+   the checked expression and sets computed to be its classifier.
 
 3. expected is non-null, create is false: check returns NULL.
 
@@ -119,14 +119,14 @@ void eat_excess(int prev) {
    was checked.
 
 We consume the reference for expected, to enable tail calls in the
-application case. 
+application case.
 
 If is_hole is NULL, then the expression parsed may not be a hole.
 Otherwise, it may be, and we will set *is_hole to true if it is
 (but leave *is_hole alone if it is not).
 
 */
-				  
+
 bool allow_run = false;
 int app_rec_level = 0;
 
@@ -143,7 +143,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 
     open_parens++;
 
-    char c = non_ws(); 
+    char c = non_ws();
     switch (c) {
     case EOF:
       report_error("Unexpected end of file.");
@@ -190,7 +190,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 		       +string("is neither \"type\" nor \"kind\".\n")
 		       +string("1. the expected classifier: ")
 		       +expected->toString());
-   if (create){ 
+   if (create){
 	  CExpr* ret = new CExpr(PI, sym, domain, range);
       ret->calc_free_in();
       return ret;
@@ -198,7 +198,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 	return 0;
       }
       else {
-         if (create){ 
+         if (create){
 	         CExpr* ret = new CExpr(PI, sym, domain, range);
             ret->calc_free_in();
             return ret;
@@ -235,7 +235,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
       symbols[id] = sym;
       symbol_types[id] = expected_domain;
 #else
-      pair<Expr *, Expr *> prevpr = 
+      pair<Expr *, Expr *> prevpr =
 	      symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain));
       Expr *prev = prevpr.first;
       Expr *prevtp = prevpr.second;
@@ -244,7 +244,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 
       //will clean up local sym name eventually
       local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) );
-      if (prev) 
+      if (prev)
 	      prev->dec();
       if (prevtp)
 	      prevtp->dec();
@@ -288,21 +288,21 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 		     +string(" a kind, not a type.\n")
 		     +string("1. The expected classifier: ")
 		     +expected->toString());
-      
+
       /* we need to map the pivar to the new sym, because in our
 	 higher-order matching we may have (_ x) to unify with t.
 	 The x must be something from an expected type, since only these
 	 can have holes.  We want to map expected vars x to computed vars y,
 	 so that we can set the hole to be \ y t, where t contains ys but
          not xs. */
-      
+
 #ifdef USE_HASH_MAPS
       Expr *prev = symbols[id];
       Expr *prevtp = symbol_types[id];
       symbols[id] = sym;
       symbol_types[id] = expected_domain;
 #else
-      pair<Expr *, Expr *> prevpr = 
+      pair<Expr *, Expr *> prevpr =
 	      symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain));
       Expr *prev = prevpr.first;
       Expr *prevtp = prevpr.second;
@@ -319,7 +319,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
         local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) );
 	      if (prev_pivar_val)
 	        prev_pivar_val->dec();
-	      if (prev) 
+	      if (prev)
 	        prev->dec();
 	      if (prevtp)
 	        prevtp->dec();
@@ -351,7 +351,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 	      orig_expected->dec();
 
 	      sym->dec(); // the pivar->val reference
-	      if (create) 
+	      if (create)
 	        return new CExpr(LAM, sym, range);
 	      sym->dec(); // the symbol table reference, otherwise in the new LAM
 	      return 0;
@@ -364,24 +364,24 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 
       Expr *code = read_code();
       //string errstr = (string("The first argument in a run expression must be")
-		    //   +string(" a call to a program.\n1. the argument: ") 
+		    //   +string(" a call to a program.\n1. the argument: ")
 		    //   +code->toString());
 
       /* determine expected type of the result term, and make sure
 	 the code term is an allowed one. */
 #if 0
       Expr *progret;
-      if (code->isArithTerm()) 
+      if (code->isArithTerm())
 	      progret = statMpz;
       else {
 	      if (code->getop() != APP)
 	        report_error(errstr);
 
 	      CExpr *call = (CExpr *)code;
-      	
+
 	      // prog is not known to be a SymExpr yet
 	      CExpr *prog = (CExpr *)call->get_head();
-      	
+
 	      if (prog->getop() != PROG)
 	        report_error(errstr);
 
@@ -389,16 +389,16 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
       }
 #else
       Expr *progret = NULL;
-      if (code->isArithTerm()) 
+      if (code->isArithTerm())
 	      progret = statMpz;
       else {
 	      if (code->getop() == APP)
         {
 	        CExpr *call = (CExpr *)code;
-        	
+
 	        // prog is not known to be a SymExpr yet
 	        CExpr *prog = (CExpr *)call->get_head();
-        	
+
 	        if (prog->getop() == PROG)
 	          progret = prog->kids[0]->get_body();
         }
@@ -433,7 +433,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 
       if (!expected)
 	      tp->inc();
- 
+
       Expr *trm = check(create, tp, NULL, NULL, return_pos);
       eat_excess(prev);
       eat_rparen();
@@ -478,14 +478,14 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
       symbols[id] = sym;
       symbol_types[id] = tp_of_trm;
 #else
-      pair<Expr *, Expr *> prevpr = 
+      pair<Expr *, Expr *> prevpr =
 	symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,tp_of_trm));
       Expr *prev = prevpr.first;
       Expr *prevtp = prevpr.second;
 #endif
 
       if (tail_calls && big_check && return_pos && !create) {
-	      if (prev) 
+	      if (prev)
 	        prev->dec();
 	      if (prevtp)
 	        prevtp->dec();
@@ -506,7 +506,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 #endif
 	      tp_of_trm->dec(); // because removed from the symbol table now
 
-	      sym->dec(); 
+	      sym->dec();
 	      return body;
       }
     }
@@ -545,7 +545,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
           report_error("Negative sign with expr that is not an int. literal.");
         }
       }
-      else 
+      else
 	      return 0;
     }
     default: { // the application case
@@ -562,7 +562,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 	      // we must clone
 	      Expr *orig_headtp = headtp;
 	      headtp = (CExpr *)headtp->clone();
-	      orig_headtp->dec(); 
+	      orig_headtp->dec();
       }
       else
 	      headtp->setcloned();
@@ -578,11 +578,11 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
       while ((c = non_ws()) != ')') {
 	our_ungetc(c);
 	if (headtp->getop() != PI)
-	  report_error(string("The type of an applied term is not ") 
+	  report_error(string("The type of an applied term is not ")
 		       + string("a pi-type.\n")
 		       + string("\n1. the type of the term: ")
 		       + headtp->toString()
-		       + (headtrm ? (string("\n2. the term: ") 
+		       + (headtrm ? (string("\n2. the term: ")
 				     + headtrm->toString())
 			  : string("")));
 	SymExpr *headtp_var = (SymExpr *)headtp->kids[0];
@@ -627,7 +627,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 			          + expected->toString()
 			          + string("\n2. The computed type: ")
 			          + headtp_range->toString()
-			          + (headtrm ? (string("\n3. the application: ") 
+			          + (headtrm ? (string("\n3. the application: ")
 					        + headtrm->toString())
 				    : string("")));
 	      expected->dec();
@@ -670,7 +670,11 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 #ifndef USE_FLAT_APP
 	      headtrm = new CExpr(APP, headtrm, arg);
 #else
+        Expr* orig_headtrm = headtrm;
         headtrm = Expr::make_app( headtrm, arg );
+        if( orig_headtrm->getclass()==CEXPR ){
+          orig_headtrm->dec();
+        }
 #endif
 	      consumed_arg = true;
 	    }
@@ -739,7 +743,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 		            + expected->toString()
 		            + string("\n2. The computed type: ")
 		            + headtp->toString()
-		            + (headtrm ? (string("\n3. the application: ") 
+		            + (headtrm ? (string("\n3. the application: ")
 				          + headtrm->toString())
 			        : string("")));
 
@@ -755,7 +759,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 	        ret = headtrm;
       }
 
-      /* do this check here to give the defeq() call above a 
+      /* do this check here to give the defeq() call above a
 	 chance to fill in some holes */
       for (int i = 0, iend = holes.size(); i < iend; i++) {
         if (!holes[i]->val){
@@ -783,7 +787,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
     report_error("Unexpected end of file.");
     break;
 
-  case '_': 
+  case '_':
     if (!is_hole)
       report_error("A hole is being used in a disallowed position.");
     *is_hole = true;
@@ -803,7 +807,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
     our_ungetc(d);
     string v;
     char c;
-    while (isdigit(c = our_getc())) 
+    while (isdigit(c = our_getc()))
       v.push_back(c);
     bool parseMpq = false;
     string v2;
@@ -811,7 +815,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
     {
       parseMpq = true;
       v.push_back( c );
-      while(isdigit(c = our_getc())) 
+      while(isdigit(c = our_getc()))
         v.push_back(c);
     }
     our_ungetc(c);
@@ -916,7 +920,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 #ifdef USE_HASH_MAPS
 void discard_old_symbol(const string &id) {
   Expr *tmp = symbols[id];
-  if (tmp) 
+  if (tmp)
     tmp->dec();
   tmp = symbol_types[id];
   if (tmp)
@@ -940,7 +944,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 
   char *f;
   if (strcmp(_filename,"stdin") == 0) {
-    curfile = stdin; 
+    curfile = stdin;
     f = strdup(_filename);
   }
   else {
@@ -967,7 +971,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
     else
       f = strdup(_filename);
     curfile = fopen(f,"r");
-    if (!curfile) 
+    if (!curfile)
       report_error(string("Could not open file \"")
 		   + string(f)
 		   + string("\" for reading.\n"));
@@ -985,15 +989,15 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
       switch ((d = non_ws())) {
       case 'd':
         char b;
-        if ((b = our_getc()) != 'e') 
+        if ((b = our_getc()) != 'e')
 	        report_error(string("Unexpected start of command."));
 
         switch ((b = our_getc())) {
           case 'f': {// expecting "define"
-	
+
 	          if (our_getc() != 'i' || our_getc() != 'n' || our_getc() != 'e')
 	            report_error(string("Unexpected start of command."));
-	
+
 	          string id(prefix_id());
 	          Expr *ttp;
 	          int prevo = open_parens;
@@ -1010,7 +1014,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 	          symbols[id] = s;
 	          symbol_types[id] = ttp;
 #else
-	          pair<Expr *, Expr *> prev = 
+	          pair<Expr *, Expr *> prev =
 	            symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp));
 	          if (prev.first)
 	            prev.first->dec();
@@ -1020,7 +1024,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 	        break;
           }
           case 'c': {// expecting "declare"
-	          if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' 
+	          if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r'
 	              || our_getc() != 'e')
 	            report_error(string("Unexpected start of command."));
 
@@ -1045,7 +1049,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 	          symbols[id] = s;
 	          symbol_types[id] = t;
 #else
-	          pair<Expr *, Expr *> prev = 
+	          pair<Expr *, Expr *> prev =
 	            symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,t));
             if( lw )
               lw->add_symbol( s, t );
@@ -1056,7 +1060,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 #endif
 	          break;
             }
-            default: 
+            default:
 	            report_error(string("Unexpected start of command."));
             } // switch((b = our_getc())) following "de"
          break;
@@ -1105,7 +1109,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
       if (our_getc() != 'p' || our_getc() != 'a' || our_getc() != 'q'
 	        || our_getc() != 'u' || our_getc() != 'e')
 	      report_error(string("Unexpected start of command."));
-	
+
       string id(prefix_id());
       Expr *ttp;
       int prevo = open_parens;
@@ -1121,7 +1125,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 	    symbols[id] = s;
 	    symbol_types[id] = ttp;
 #else
-	    pair<Expr *, Expr *> prev = 
+	    pair<Expr *, Expr *> prev =
 	      symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp));
 	    if (prev.first)
 	      prev.first->dec();
@@ -1150,7 +1154,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
         break;
       }
       case 'p': { // program case
-        if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g' 
+        if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g'
 	         || our_getc() != 'r' || our_getc() != 'a' || our_getc() != 'm')
 	        report_error(string("Unexpected start of command."));
 
@@ -1209,10 +1213,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
 	        symbols->insert(varstr.c_str(), pair<Expr *, Expr *>(var,tp));
 #endif
         }
-      
+
         if (!vars.size())
 	        report_error("A program lacks input variables.");
-   
+
         statType->inc();
         int prev = open_parens;
         Expr *progtp = check(true,statType,&tmp,0, true);
@@ -1221,7 +1225,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
         if (!progtp->isDatatype())
 	        report_error(string("Return type for a program is not a")
 		            +string(" datatype.\n1. the type: ")+progtp->toString());
-        
+
         Expr *progcode = read_code();
 
         for (int i = vars.size() - 1, iend = 0; i >= iend; i--) {
@@ -1231,10 +1235,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
         }
 
         // just put the type here for type checking.  Make sure progtp is kid 0.
-        prog->val = new CExpr(PROG, progtp); 
-        
+        prog->val = new CExpr(PROG, progtp);
+
         check_code(progcode);
-     
+
         progcode = new CExpr(PROG, progtp, new CExpr(PROGVARS, vars), progcode);
         //if compiling side condition code, give this code to the side condition code writer
         if( a.compile_scc ){
@@ -1242,7 +1246,7 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
             scw->add_scc( progstr, (CExpr*)progcode );
           }
         }
-	
+
 	// remove the variables from the symbol table.
         for (int i = 0, iend = vars.size(); i < iend; i++) {
 	        string &s = ((SymSExpr *)vars[i])->s;
@@ -1263,10 +1267,10 @@ void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
         break;
       }
 
-      default: 
+      default:
 	      report_error(string("Unexpected start of command."));
       } // switch((d = non_ws())
-        
+
       eat_char(')');
     } // while
     else
@@ -1350,7 +1354,7 @@ void cleanup() {
   delete symbols;
 #endif
 
-  // clean up programs 
+  // clean up programs
 
   symmap2::iterator j, jend;
   for (j = progs.begin(), jend = progs.end(); j != jend; j++) {
@@ -1378,6 +1382,6 @@ void init() {
   symbols->insert("type", pair<Expr *, Expr *>(statType, statKind));
   statType->inc();
   symbols->insert("mpz", pair<Expr *, Expr *>(statMpz, statType));
-  symbols->insert("mpq", pair<Expr *, Expr *>(statMpq, statType)); 
+  symbols->insert("mpq", pair<Expr *, Expr *>(statMpq, statType));
 #endif
 }
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
index 225700580..34c6c133b 100644
--- a/proofs/lfsc_checker/code.cpp
+++ b/proofs/lfsc_checker/code.cpp
@@ -23,7 +23,7 @@ string *eat_str(const char *str, bool check_end = true) {
     our_ungetc(d);
     return s;
   }
-   
+
   delete s;
   return 0;
 }
@@ -76,13 +76,17 @@ Expr *read_case() {
 	    prevs.push_back(symbols[varstr]);
 	    symbols[varstr] = var;
 #else
-	    prevs.push_back(symbols->insert(varstr.c_str(), 
+	    prevs.push_back(symbols->insert(varstr.c_str(),
 					    pair<Expr *, Expr *>(var,NULL)));
 #endif
 #ifndef USE_FLAT_APP
 	    pat = new CExpr(APP,pat,var);
 #else
+      Expr* orig_pat = pat;
       pat = Expr::make_app(pat,var);
+      if( orig_pat->getclass()==CEXPR ){
+        orig_pat->dec();
+      }
 #endif
     }
     break;
@@ -101,7 +105,7 @@ Expr *read_case() {
     pat = read_ctor();
     break;
   }
-  
+
   Expr *ret = read_code();
   if( pat )
     ret = new CExpr(CASE, pat, ret);
@@ -124,16 +128,16 @@ Expr *read_code() {
   string *pref = NULL;
   char d = non_ws();
   switch(d) {
-    case '(': 
+    case '(':
     {
-      char c = non_ws(); 
-      switch (c) 
+      char c = non_ws();
+      switch (c)
       {
-        case 'd': 
+        case 'd':
         {
           our_ungetc('d');
           pref = eat_str("do");
-          if (pref) 
+          if (pref)
 	          break;
           Expr *ret = read_code();
           while ((c = non_ws()) != ')') {
@@ -142,11 +146,11 @@ Expr *read_code() {
           }
           return ret;
         }
-        case 'f': 
+        case 'f':
         {
           our_ungetc('f');
           pref = eat_str("fail");
-          if (pref) 
+          if (pref)
 	          break;
 
           Expr *c = read_code();
@@ -156,14 +160,14 @@ Expr *read_code() {
           //if (c->getclass() != SYMS_EXPR || ((SymExpr *)c)->val)
 	         // report_error(string("\"fail\" must be used with a (undefined) base ")
 		        //  +string("type.\n1. the expression used: "+c->toString()));
-          
+
           return new CExpr(FAIL, c);
         }
-        case 'l': 
+        case 'l':
         {
           our_ungetc('l');
           pref = eat_str("let");
-          if (pref) 
+          if (pref)
 	          break;
 
           string id(prefix_id());
@@ -175,12 +179,12 @@ Expr *read_code() {
           Expr *prev = symbols[id];
           symbols[id] = var;
 #else
-          pair<Expr *, Expr *> prev = 
+          pair<Expr *, Expr *> prev =
 	          symbols->insert(id.c_str(), pair<Expr *, Expr *>(var,NULL));
 #endif
 
           Expr *t2 = read_code();
-      
+
 #ifdef USE_HASH_MAPS
           symbols[id] = prev;
 #else
@@ -189,11 +193,11 @@ Expr *read_code() {
           eat_char(')');
           return new CExpr(LET, var, t1, t2);
         }
-        case 'i': 
+        case 'i':
         {
           our_ungetc('i');
           pref = eat_str("ifmarked",false);
-          if (pref) 
+          if (pref)
 	          break;
 #ifndef MARKVAR_32
           Expr *e1 = read_code();
@@ -220,16 +224,16 @@ Expr *read_code() {
           eat_char(')');
           return ret;
         }
-        case 'm': 
+        case 'm':
         {
           char c;
-          switch ((c = our_getc())) 
+          switch ((c = our_getc()))
           {
-            case 'a': 
+            case 'a':
             {
 	            char cc;
 	            switch ((cc = our_getc())) {
-	              case 't': 
+	              case 't':
                 {
 	                our_ungetc('t');
 	                pref = eat_str("tch");
@@ -253,7 +257,7 @@ Expr *read_code() {
                   }
 	                return new CExpr(MATCH,cases);
                 }
-	              case 'r': 
+	              case 'r':
                 {
 	                our_ungetc('r');
 	                pref = eat_str("rkvar", false);
@@ -268,7 +272,7 @@ Expr *read_code() {
                   CExpr* ret = NULL;
                   if( index>=1 && index<=32 )
                   {
-                    ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() ); 
+                    ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() );
                   }
                   else
                   {
@@ -287,7 +291,7 @@ Expr *read_code() {
 	                break;
               }
             }
-            case 'p': 
+            case 'p':
             {
 	            our_ungetc('p');
 	            pref = eat_str("p_",false);
@@ -297,7 +301,7 @@ Expr *read_code() {
               }
 	            char c = our_getc();
 	            switch(c) {
-	            case 'a': 
+	            case 'a':
               {
 	              our_ungetc('a');
 	              pref = eat_str("add");
@@ -311,7 +315,7 @@ Expr *read_code() {
 	              eat_char(')');
 	              return ret;
 	            }
-	            case 'n': 
+	            case 'n':
               {
 	              our_ungetc('n');
 	              pref = eat_str("neg");
@@ -319,12 +323,12 @@ Expr *read_code() {
 	                pref->insert(0,"mp_");
 	                break;
 	              }
-            	  
+
 	              Expr *ret = new CExpr(NEG, read_code());
 	              eat_char(')');
 	              return ret;
 	            }
-	            case 'i': 
+	            case 'i':
               {	// mpz_if_neg
                 char c = our_getc();
                 if( c=='f' )
@@ -439,7 +443,7 @@ Expr *read_code() {
         {
           our_ungetc('c');
           pref = eat_str("compare");
-          if (pref) 
+          if (pref)
 	          break;
           Expr *e1 = read_code();
           Expr *e2 = read_code();
@@ -452,21 +456,21 @@ Expr *read_code() {
         case EOF:
           report_error("Unexpected end of file.");
           break;
-        default: 
+        default:
         { // the application case
           our_ungetc(c);
           break;
         }
       }
       // parse application
-      if (pref) 
+      if (pref)
         // we have eaten part of the name of an applied identifier
         pref->append(prefix_id());
       else
         pref = new string(prefix_id());
 
       Expr *ret = progs[*pref];
-      if (!ret) 
+      if (!ret)
 #ifdef USE_HASH_TABLES
         ret = symbols[*pref];
 #else
@@ -486,7 +490,11 @@ Expr *read_code() {
         ret = new CExpr(APP,ret,read_code());
 #else
         Expr* ke = read_code();
+        Expr* orig_ret = ret;
         ret = Expr::make_app(ret,ke);
+        if( orig_ret->getclass()==CEXPR ){
+          orig_ret->dec();
+        }
 #endif
         }
       return ret;
@@ -494,7 +502,7 @@ Expr *read_code() {
     case EOF:
       report_error("Unexpected end of file.");
       break;
-    case '_': 
+    case '_':
       report_error("Holes may not be used in code.");
       return NULL;
     case '0':
@@ -506,19 +514,19 @@ Expr *read_code() {
     case '6':
     case '7':
     case '8':
-    case '9': 
+    case '9':
     {
       our_ungetc(d);
       string v;
       char c;
-      while (isdigit(c = our_getc())) 
+      while (isdigit(c = our_getc()))
         v.push_back(c);
       bool parseMpq = false;
       if( c=='/' )
       {
         parseMpq = true;
         v.push_back(c);
-        while(isdigit(c = our_getc())) 
+        while(isdigit(c = our_getc()))
           v.push_back(c);
       }
       our_ungetc(c);
@@ -540,7 +548,7 @@ Expr *read_code() {
         return new IntExpr(num);
       }
     }
-    default: 
+    default:
     {
       our_ungetc(d);
       string id(prefix_id());
@@ -550,7 +558,7 @@ Expr *read_code() {
       pair<Expr *, Expr *> p = symbols->get(id.c_str());
       Expr *ret = p.first;
 #endif
-      if (!ret) 
+      if (!ret)
         ret = progs[id];
       if (!ret)
         report_error(string("Undeclared identifier: ")+id);
@@ -609,7 +617,7 @@ Expr *check_code(Expr *_e) {
 
     int iend = args.size();
     vector<Expr *> argtps(iend);
-    for (int i = 0; i < iend; i++) 
+    for (int i = 0; i < iend; i++)
       argtps[i] = check_code(args[i]);
 #endif
 
@@ -623,18 +631,18 @@ Expr *check_code(Expr *_e) {
       tp = symbols->get(((SymSExpr *)h)->s.c_str()).second;
 #endif
     }
-    
+
     if (!tp)
       report_error(string("The head of an application is missing a type in ")
 		   +string("code.\n1. the application: ")+e->toString());
-    
+
     tp = tp->followDefs();
 
     if (tp->getop() != PI)
       report_error(string("The head of an application does not have ")
 		   +string("functional type in code.")
 		   +string("\n1. the application: ")+e->toString());
-    
+
     CExpr *cur = (CExpr *)tp;
     int i = 0;
     while (cur->getop() == PI) {
@@ -661,7 +669,7 @@ Expr *check_code(Expr *_e) {
 		          + string("\n5. expected type: ")
 		          +cur->kids[1]->toString());
       }
-      
+
       //if (cur->kids[2]->free_in((SymExpr *)cur->kids[0]))
       if( cur->get_free_in() ){
         cur->calc_free_in();
@@ -682,8 +690,8 @@ Expr *check_code(Expr *_e) {
 		   +string("arguments in code.\n")
 		   +string("1. the application: ")+e->toString()
 		   +string("\n2. the head's type: ")+tp->toString());
-      
-    
+
+
     return cur;
   }
   //is this right?
@@ -693,7 +701,7 @@ Expr *check_code(Expr *_e) {
   case MPQ:
     return statType;
     break;
-  case DO: 
+  case DO:
     check_code(e->kids[0]);
     return check_code(e->kids[1]);
 
@@ -706,22 +714,22 @@ Expr *check_code(Expr *_e) {
     Expr *prevtp = symbol_types[var->s];
     symbol_types[var->s] = tp1;
 #else
-    pair<Expr *, Expr *> prev = 
+    pair<Expr *, Expr *> prev =
       symbols->insert(var->s.c_str(), pair<Expr *, Expr *>(NULL,tp1));
 #endif
 
     Expr *tp2 = check_code(e->kids[2]);
-      
+
 #ifdef USE_HASH_MAPS
     symbol_types[var->s] = prevtp;
 #else
     symbols->insert(var->s.c_str(), prev);
 #endif
-    
+
     return tp2;
   }
 
-  case ADD: 
+  case ADD:
   case MUL:
   case DIV:
   {
@@ -732,14 +740,14 @@ Expr *check_code(Expr *_e) {
       report_error(string("Argument to mp_[arith] does not have type \"mpz\" or \"mpq\".\n")
 		   +string("1. the argument: ")+e->kids[0]->toString()
 		   +string("\n1. its type: ")+tp0->toString());
-    
+
     if (tp0 != tp1)
       report_error(string("Arguments to mp_[arith] have differing types.\n")
 		   +string("1. argument 1: ")+e->kids[0]->toString()
 		   +string("\n1. its type: ")+tp0->toString()
 		   +string("2. argument 2: ")+e->kids[1]->toString()
 		   +string("\n2. its type: ")+tp1->toString());
-    
+
     return tp0;
   }
 
@@ -749,18 +757,18 @@ Expr *check_code(Expr *_e) {
       report_error(string("Argument to mp_neg does not have type \"mpz\" or \"mpq\".\n")
 		   +string("1. the argument: ")+e->kids[0]->toString()
 		   +string("\n1. its type: ")+tp0->toString());
-    
+
     return tp0;
   }
 
-  case IFNEG: 
+  case IFNEG:
   case IFZERO: {
     Expr *tp0 = check_code(e->kids[0]);
     if (tp0 != statMpz && tp0 != statMpq)
       report_error(string("Argument to mp_if does not have type \"mpz\" or \"mpq\".\n")
 		   +string("1. the argument: ")+e->kids[0]->toString()
 		   +string("\n1. its type: ")+tp0->toString());
-    
+
     SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]);
     SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]);
     if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2)
@@ -785,7 +793,7 @@ Expr *check_code(Expr *_e) {
   }
   case MARKVAR: {
     SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]);
-  
+
     Expr* tptp = NULL;
 
     if (tp->getclass() == SYMS_EXPR && !tp->val){
@@ -808,12 +816,12 @@ Expr *check_code(Expr *_e) {
     return tp;
   }
 
-  case IFMARKED: 
+  case IFMARKED:
   {
     SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]);
 
     Expr* tptp = NULL;
-   
+
     if (tp->getclass() == SYMS_EXPR && !tp->val){
 #ifdef USE_HASH_MAPS
       tptp = symbol_types[tp->s];
@@ -821,7 +829,7 @@ Expr *check_code(Expr *_e) {
       tptp = symbols->get(tp->s.c_str()).second;
 #endif
     }
-    
+
     if (!tptp->isType( statType ) ){
       string errstr = (string("\"ifmarked\" is used with an expression which ")
 		      +string("cannot be a lambda-bound variable.\n")
@@ -877,7 +885,7 @@ Expr *check_code(Expr *_e) {
 		   +string("\n4. second expression's type: ")+tp3->toString());
     return tp2;
   }
-  case MATCH: 
+  case MATCH:
   {
     SymSExpr *scruttp = (SymSExpr *)check_code(e->kids[0]);
     Expr *tptp = NULL;
@@ -905,14 +913,14 @@ Expr *check_code(Expr *_e) {
     while ((c_or_default = *cur++)) {
       Expr *tp = NULL;
       CExpr *pat = NULL;
-      if (c_or_default->getop() != CASE) 
+      if (c_or_default->getop() != CASE)
         // this is the default of the MATCH
         tp = check_code(c_or_default);
       else {
         // this is a CASE of the MATCH
         c = (CExpr *)c_or_default;
         pat = (CExpr *)c->kids[0]; // might be just a SYMS_EXPR
-        if (pat->getclass() == SYMS_EXPR) 
+        if (pat->getclass() == SYMS_EXPR)
           tp = check_code(c->kids[1]);
         else {
           // extend type context and then check the body of the case
@@ -941,7 +949,7 @@ Expr *check_code(Expr *_e) {
             symbol_types[((SymSExpr *)vars[i])] = curtp->followDefs()->kids[1];
 #else
             prevs.push_back
-              (symbols->insert(((SymSExpr *)vars[i])->s.c_str(), 
+              (symbols->insert(((SymSExpr *)vars[i])->s.c_str(),
                                pair<Expr *, Expr *>(NULL,
                                                     ((CExpr *)(curtp->followDefs()))->kids[1])));
 #endif
@@ -949,7 +957,7 @@ Expr *check_code(Expr *_e) {
           }
 
           tp = check_code(c->kids[1]);
-	
+
           for (int i = 0, iend = prevs.size(); i < iend; i++) {
 #ifdef USE_HASH_MAPS
             symbol_types[((SymSExpr *)vars[i])->s] = prevs[i];
@@ -974,13 +982,13 @@ Expr *check_code(Expr *_e) {
                          : (string("\n2. type for the body of case for ")
                             +pat->toString()))
                        +string(": ")+tp->toString());
-      
+
     }
 
     return mtp;
               }
   } // end switch
-   
+
   report_error("Type checking an unrecognized form of code (internal error).");
   return NULL;
 }
@@ -1013,12 +1021,12 @@ Expr *run_code(Expr *_e) {
       return e;
     case HOLE_EXPR: {
       Expr *tmp = e->followDefs();
-      if (tmp == e) 
+      if (tmp == e)
 	      report_error("Encountered an unfilled hole running code.");
       tmp->inc();
       return tmp;
     }
-    case SYMS_EXPR: 
+    case SYMS_EXPR:
     case SYM_EXPR: {
       Expr *tmp = e->followDefs();
       //std::cout << "follow def = ";
@@ -1054,7 +1062,7 @@ Expr *run_code(Expr *_e) {
     r0->dec();
     return r1;
   }
-  case ADD: 
+  case ADD:
   case MUL:
   case DIV:
   {
@@ -1127,7 +1135,7 @@ Expr *run_code(Expr *_e) {
       return NULL;
     }
   }
-  case IFNEG: 
+  case IFNEG:
   case IFZERO:{
     Expr *r1 = run_code(e->kids[0]);
     if (!r1)
@@ -1142,7 +1150,7 @@ Expr *run_code(Expr *_e) {
     }else if( r1->getclass() == RAT_EXPR ){
       if( e->getop() == IFNEG )
         cond = mpq_sgn( ((RatExpr *)r1)->n )<0;
-      else if( e->getop() == IFZERO ) 
+      else if( e->getop() == IFZERO )
         cond = mpq_sgn( ((RatExpr *)r1)->n )==0;
     }
     else
@@ -1203,7 +1211,7 @@ Expr *run_code(Expr *_e) {
       _e = e->kids[2];
       goto start_run_code;
     }
-    //else 
+    //else
     r2->dec();
     _e = e->kids[3];
     goto start_run_code;
@@ -1283,7 +1291,7 @@ Expr *run_code(Expr *_e) {
 
     vector<Expr *> args;
     Expr *hd = e->collect_args(args);
-    for (int i = 0, iend = args.size(); i < iend; i++) 
+    for (int i = 0, iend = args.size(); i < iend; i++)
       if (!(args[i] = run_code(args[i]))) {
 	      for (int j = 0; j < i; j++)
 	         args[j]->dec();
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 7ffc6469a..ae0e49531 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -234,6 +234,7 @@ Expr* Expr::make_app(Expr* e1, Expr* e2 )
       counter = 0;
       while( ((CExpr*)e1)->kids[counter] ){
          ret->kids[counter] = ((CExpr*)e1)->kids[counter];
+         ret->kids[counter]->inc();
          counter++;
       }
       ret->kids[counter] = e2;
@@ -346,8 +347,8 @@ Expr* CExpr::convert_to_tree_app( Expr* e )
   if( e->getop()==APP )
   {
     std::vector< Expr* > kds;
-    int counter = 1;
-    while( ((CExpr*)e)->kids[counter] )
+    int counter = 1;
+    while( ((CExpr*)e)->kids[counter] )
     {
       kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) );
       counter++;
@@ -963,4 +964,4 @@ void SymExpr::smark( int m )
 {
   mark_map[this] = m;
 }
-#endif
\ No newline at end of file
+#endif
diff --git a/proofs/signatures/ex-mem.plf b/proofs/signatures/ex-mem.plf
new file mode 100755
index 000000000..12c4c3e16
--- /dev/null
+++ b/proofs/signatures/ex-mem.plf
@@ -0,0 +1,68 @@
+; AJR : proof used for testing memory use of theory lemmas
+
+(check
+(% s sort
+(% a (term s)
+(% b (term s)
+(% c (term s)
+(% f (term (arrow s s))
+
+; -------------------- declaration of input formula -----------------------------------
+
+(% A1 (th_holds (= s a b))
+(% A2 (th_holds (= s b a))
+(% A3 (th_holds (not (= s a a)))
+
+; ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
+
+(decl_atom (= s a b) (\ v1 (\ a1
+(decl_atom (= s b a) (\ v2 (\ a2
+(decl_atom (= s a a) (\ v3 (\ a3
+
+; --------------------------- proof of theory lemma ---------------------------------------------
+
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT2
+(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3  (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT3
+;...add copies here...
+
+; -------------------- clausification of input formulas -----------------------------------------
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(clausify_false
+  (contra _ A1 l1)
+))) (\ C1
+; C1 is the clause ( v1 )
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+   (contra _ A2 l2)
+))) (\ C2
+; C2 is the clause ( v2 )
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(clausify_false
+  (contra _ l3 A3)
+))) (\ C3
+; C3 is the clause ( ~v3 )
+
+
+; -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _
+(R _ _ C2
+(R _ _ C1 CT1 v1) v2) C3 v3)
+
+(\ x x))
+
+)))))))))))))))))))))))))))))
+))