Index: scrambler.cpp
===================================================================
--- scrambler.cpp	(revision 573)
+++ scrambler.cpp	(working copy)
@@ -48,6 +48,17 @@
 bool no_scramble = false;
 bool scramble_named_annot = false;
 bool lift_named_annot = false;
+/**
+ * If set to true the following modifications will be made addionally.
+ * 1. The following command will be prepended.
+ *   (set-option :produce-unsat-cores true)
+ * 2. An (get-unsat-core) command will be added after each (check-sat)
+ *    command.
+ * 3. Each (assert fmla) will be replaced by
+ *    (assert (! fmla) :named freshId)
+ * where "freshId" is some newly constructed identifier.
+ */
+bool generate_unsat_core_benchmark = false;
 
 typedef std::tr1::unordered_map<std::string, std::string> NameMap;
 NameMap names;
@@ -459,7 +470,7 @@
 
 void print_node(std::ostream &out, node *n, bool keep_annontations)
 {
-    if (!no_scramble && !keep_annontations && n->symbol == "!") {
+    if (!keep_annontations && n->symbol == "!") {
         print_node(out, n->children[0], keep_annontations);
     } else {
         std::string name;
@@ -501,6 +512,9 @@
                 out << n->symbol;
             }
         }
+        if (generate_unsat_core_benchmark && n->symbol == "assert") {
+        	name = make_annot_name(name_idx++);
+        }
         if (!name.empty()) {
             out << " (!";
         }
@@ -522,6 +536,10 @@
         if (n->needs_parens) {
             out << ')';
         }
+        if (generate_unsat_core_benchmark && n->symbol == "check-sat") {
+        	// append get-unsat-core after check-sat
+        	std::cout << std::endl << "(get-unsat-core)";
+        }
     }
 }
 
@@ -721,7 +739,8 @@
               << "  -unfold_end N\n"
               << "  -core NAMES_FILE\n"
               << "  -scramble_named_annot [true|false]\n"
-              << "  -lift_named_annot [true|false]\n";
+              << "  -lift_named_annot [true|false]\n"
+              << "  -generate_unsat_core_benchmark [true|false]\n";
     std::cout.flush();
     exit(1);
 }
@@ -895,6 +914,15 @@
                 usage(argv[0]);
             }
             i += 2;
+        } else if (strcmp(argv[i], "-generate_unsat_core_benchmark") == 0 && i+1 < argc) {
+            if (strcmp(argv[i+1], "true") == 0) {
+                generate_unsat_core_benchmark = true;
+            } else if (strcmp(argv[i+1], "false") == 0) {
+            	generate_unsat_core_benchmark = false;
+            } else {
+                usage(argv[0]);
+            }
+            i += 2;
         } else {
             usage(argv[0]);
         }
@@ -910,6 +938,11 @@
         }
     }
 
+    if (generate_unsat_core_benchmark) {
+    	// prepend command that enables production of unsat-cores
+    	std::cout << "(set-option :produce-unsat-cores true)"  << std::endl;
+    }
+
     while (!std::cin.eof()) {
         yyparse();
         if (!unfold) {