Under option

src/expr_parser.cpp

@@ -174,8 +174,10 @@ Expr ExprParser::parseExpr()
               // construct fresh variables.
               // If d_isReference is false, we lookup the variables in the
               // specified list.
+              // This is overriden if the option d_binderFresh is true.
+              bool isLookup = !d_state.getOptions().d_binderFresh && !d_isReference;
               d_state.pushScope();
-              std::vector<Expr> vs = parseAndBindSortedVarList(!d_isReference);
+              std::vector<Expr> vs = parseAndBindSortedVarList(isLookup);
               if (vs.empty())
               {
                 d_lex.parseError("Expected non-empty sorted variable list");

src/main.cpp

@@ -24,7 +24,11 @@ int main( int argc, char* argv[] )
   {
     std::string arg(argv[i]);
     i++;
-    if (arg=="--gen-compile")
+    if (arg=="--binder-fresh")
+    {
+      opts.d_binderFresh = true;
+    }
+    else if (arg=="--gen-compile")
     {
       opts.d_compile = true;
     }
@@ -56,6 +60,7 @@ int main( int argc, char* argv[] )
     else if (arg=="--help")
     {
       std::stringstream out;
+      out << "     --binder-fresh: binders generate fresh variables when parsed in proof files." << std::endl;
       out << "      --gen-compile: output the C++ code for all included signatures from the input file." << std::endl;
       out << "             --help: displays this message." << std::endl;
       out << " --no-normalize-dec: do not treat decimal literals as syntax sugar for rational literals." << std::endl;

src/state.cpp

@@ -18,6 +18,7 @@ Options::Options()
   d_ruleSymTable = true;
   d_normalizeDecimal = true;
   d_normalizeHexadecimal = true;
+  d_binderFresh = false;
 }
 
 State::State(Options& opts, Stats& stats)

src/state.h

@@ -29,6 +29,8 @@ class Options
   bool d_ruleSymTable;
   bool d_normalizeDecimal;
   bool d_normalizeHexadecimal;
+  /** Binders generate fresh variables in proof files */
+  bool d_binderFresh;
 };
 
 /**