diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index de1b7060898..a052ce716c2 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/c_preprocess.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/pass_preprocess.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
@@ -339,6 +340,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
+  if(cmdline.isset("pass"))
+  {
+    options.set_option("pass", true);
+  }
+
   if(cmdline.isset("max-node-refinement"))
     options.set_option("max-node-refinement", cmdline.get_value("max-node-refinement"));
 
@@ -454,6 +460,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));
 
+  options.set_option("pass", cmdline.isset("pass"));
+
   if(cmdline.isset("graphml-witness"))
   {
     options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
@@ -913,6 +921,12 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);
 
+    if(cmdline.isset("pass"))
+    {
+      status() << "PASS Preprocessing " << eom;
+      pass_preprocess(symbol_table, goto_functions);
+    }
+
     // remove returns, gcc vectors, complex
     remove_returns(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
@@ -997,6 +1011,7 @@ bool cbmc_parse_optionst::process_goto_program(
     // remove skips
     remove_skip(goto_functions);
     goto_functions.update();
+
   }
 
   catch(const char *e)
@@ -1188,6 +1203,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
+    " --pass                       use parameterized array for string solving (experimental)\n"
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n"
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 16ea202ba8c..59ff788b0a3 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -36,7 +36,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(fixedbv)" \
-  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)" \
+  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)(pass)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 95d9b35cf38..8595a26871c 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
+#include <solvers/refinement/string_refinement.h>
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
 #include <solvers/cvc/cvc_dec.h>
@@ -324,6 +325,29 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
 
 /*******************************************************************\
 
+Function: cbmc_solverst::get_string_refinement
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+ 
+cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
+{
+  propt *prop;
+  prop=new satcheck_no_simplifiert();
+  prop->set_message_handler(get_message_handler());
+
+  string_refinementt *string_refinement = new string_refinementt(ns, *prop);
+  string_refinement->set_ui(ui);
+  return new cbmc_solver_with_propt(string_refinement, prop);
+}
+
+/*******************************************************************\
+
 Function: cbmc_solverst::get_smt1
 
   Inputs:
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
index 765b3bbfd13..0096f140ffe 100644
--- a/src/cbmc/cbmc_solvers.h
+++ b/src/cbmc/cbmc_solvers.h
@@ -84,6 +84,8 @@ class cbmc_solverst:public messaget
       solver = get_dimacs();
     else if(options.get_bool_option("refine"))
       solver = get_bv_refinement();
+    else if(options.get_bool_option("pass"))
+      solver = get_string_refinement();
     else if(options.get_bool_option("smt1"))
       solver = get_smt1(get_smt1_solver_type());
     else if(options.get_bool_option("smt2"))
@@ -111,6 +113,7 @@ class cbmc_solverst:public messaget
   solvert* get_default();
   solvert* get_dimacs();
   solvert* get_bv_refinement();
+  solvert* get_string_refinement();
   solvert* get_smt1(smt1_dect::solvert solver);
   solvert* get_smt2(smt2_dect::solvert solver);