diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml
index 50fb48738fbe4bd9b852fe9b78db33c0bde3217b..388572b8c04b69c8d47657d15717c4b3c8c7fb22 100644
--- a/src/driver/call_provers.ml
+++ b/src/driver/call_provers.ml
@@ -347,7 +347,7 @@ let result_buffer : (server_id, prover_result) Hashtbl.t = Hashtbl.create 17
 let call_on_file ~command ~limit ~res_parser ~printer_mapping
                  ?(inplace=false) fin () =
   let id = gen_id () in
-  let cmd, _, on_timelimit =
+  let cmd, use_stdin, on_timelimit =
     actualcommand ~cleanup:true ~inplace command limit fin in
   let limit = adapt_limits limit on_timelimit in
   let save =
@@ -359,7 +359,7 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping
   Hashtbl.add saved_data id save;
   let timelimit = get_time limit in
   let memlimit = get_mem limit in
-  Prove_client.send_request ~id ~timelimit ~memlimit ~cmd;
+  Prove_client.send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd;
   ServerCall id
 
 let get_new_results ~blocking =
diff --git a/src/driver/prove_client.ml b/src/driver/prove_client.ml
index ef29dfdcc4c04762884058ac182891333c63eb18..7e530d4230e1fd5eae123c7bcfddd115805c8888 100644
--- a/src/driver/prove_client.ml
+++ b/src/driver/prove_client.ml
@@ -92,10 +92,11 @@ let set_max_running_provers x =
   if !socket <> None then
     send_request_string ("parallel;" ^ string_of_int x)
 
-let send_request ~id ~timelimit ~memlimit ~cmd =
+let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd =
   force_connect ();
   let buf = Buffer.create 128 in
-  Buffer.add_string buf "run;";
+  let servercommand = if use_stdin then "runstdin;" else "run;" in
+  Buffer.add_string buf servercommand;
   Buffer.add_string buf (string_of_int id);
   Buffer.add_char buf ';';
   Buffer.add_string buf (string_of_int timelimit);
diff --git a/src/driver/prove_client.mli b/src/driver/prove_client.mli
index d933dada61597684998794558d5a1be965c675ef..d7a14a73c09c1e7a6f032789fd2e2d32c2dbdb1e 100644
--- a/src/driver/prove_client.mli
+++ b/src/driver/prove_client.mli
@@ -6,6 +6,7 @@ val set_max_running_provers : int -> unit
 val connect : unit -> unit
 
 val send_request :
+ use_stdin:bool ->
  id:int ->
  timelimit:int ->
  memlimit:int ->
diff --git a/src/server/README.server b/src/server/README.server
index 32b6a63ebbed26939ddfbc824402e0be5947e933..e89eac6413eb6b5e25594a15e506a88fb1054976 100644
--- a/src/server/README.server
+++ b/src/server/README.server
@@ -20,7 +20,7 @@ A client request is a single line which looks like this:
   commandkind;payload
 
 Where commandkind is a simple string and payload is a semicolon-separated
-list. There are currently only two possible commands. The first command looks
+list. There are currently three possible commands. The first command looks
 like this:
 
   run;id;timeout;memlimit;cmd;arg1;arg2;...;argn
@@ -52,7 +52,16 @@ Their meaning is the following:
   file     - the path to a file which contains the stdout and stderr of the
              executed program
 
-The second commmand is like this:
+The second command is very similar:
+
+  runstdin;id;timeout;memlimit;cmd;arg1;arg2;...;argn;filename
+
+The meaning of this command is identical to the "run" command, with the
+difference that an extra filename is given as the last argument to the
+command. This filename is not passed to the command as a commandline argument,
+instead it is "piped" into the stdin of the command.
+
+The third commmand is like this:
 
   parallel;num
 
diff --git a/src/server/request.c b/src/server/request.c
index 866ddd791d89e73a5008490f1a12b4de3cf5189f..8ef2fe700c99b9b36a51bdf11a72588196527f44 100644
--- a/src/server/request.c
+++ b/src/server/request.c
@@ -49,6 +49,7 @@ prequest parse_request(char* str_req, int len, int key) {
   int pos = 0;
   prequest req;
   char* tmp;
+  bool runstdin = false;
 
   semic = count_semicolons(str_req, len);
   if (semic == 0) {
@@ -73,11 +74,16 @@ prequest parse_request(char* str_req, int len, int key) {
   }
   pos = copy_up_to_semicolon(str_req, pos, len, &tmp);
   if (strncmp(tmp, "run", pos) != 0) {
-    return NULL;
+    if (strncmp(tmp, "runstdin", pos) == 0) {
+      runstdin = true;
+    } else {
+      return NULL;
+    }
   }
   req = (prequest) malloc(sizeof(request));
   req->key = key;
   req->numargs = numargs;
+  req->usestdin = runstdin;
   pos = copy_up_to_semicolon(str_req, pos, len, &(req->id));
   pos = copy_up_to_semicolon(str_req, pos, len, &tmp);
   req->timeout = atoi(tmp);
diff --git a/src/server/request.h b/src/server/request.h
index ff96bfcbb230ee8c1fc92da0d729124a11609078..0e174e0af93396ecdcf3479e7a9c34dbdf6aaf15 100644
--- a/src/server/request.h
+++ b/src/server/request.h
@@ -1,11 +1,14 @@
 #ifndef REQUEST_H
 #define REQUEST_H
 
+#include <stdbool.h>
+
 typedef struct {
   int key;
   char* id;
   int timeout;
   int memlimit;
+  bool usestdin;
   char* cmd;   // the command to execute
   int numargs; // the length of the following array
   char** args; // the arguments of the process to run (not including the command)
diff --git a/src/server/server-unix.c b/src/server/server-unix.c
index aa5b601b2627947df78aff304fe68a6ce9b6168b..21ac85ba214aebbcadd7b021bb21cded29442a77 100644
--- a/src/server/server-unix.c
+++ b/src/server/server-unix.c
@@ -241,12 +241,19 @@ void queue_write(pclient client, char* msgbuf) {
 pid_t create_process(char* cmd,
                      int argc,
                      char** argv,
+                     bool usestdin,
                      int outfile,
                      int timelimit,
                      int memlimit) {
   struct rlimit res;
   int i;
   char** unix_argv;
+  int count = argc;
+  // in the case of usestdin, the last argument is in fact not passed to
+  // execvp, it contains the filename instead
+  if (usestdin) {
+    count--;
+  }
   unix_argv = (char**)malloc(sizeof(char*) * (argc + 2));
   unix_argv[0] = cmd;
   unix_argv[argc + 1] = NULL;
@@ -292,6 +299,9 @@ pid_t create_process(char* cmd,
   //adapt stdout/stderr
   dup2(outfile, 1);
   dup2(outfile, 2);
+  if (usestdin) {
+    freopen(argv[argc-1], "r", stdin);
+  }
 
   /* execute the command */
   execvp(cmd,unix_argv);
@@ -405,6 +415,7 @@ void run_request (prequest r) {
   id = create_process(r->cmd,
                       r->numargs,
                       r->args,
+                      r->usestdin,
                       out_descr,
                       r->timeout,
                       r->memlimit);
diff --git a/src/server/server-win.c b/src/server/server-win.c
index b1be8fd0f4094be79e6746b37ed37d9731f6aa23..8357e7e71fda72df1b968f966aacc626251ad422 100644
--- a/src/server/server-win.c
+++ b/src/server/server-win.c
@@ -224,13 +224,20 @@ void run_request (prequest r) {
    char* outfile;
    pproc proc;
    int key;
+   int argcount = r->numargs;
    JOBOBJECT_EXTENDED_LIMIT_INFORMATION limits;
    JOBOBJECT_ASSOCIATE_COMPLETION_PORT portassoc;
    STARTUPINFO si;
-   HANDLE ghJob, outfilehandle;
+   HANDLE ghJob, outfilehandle, infilehandle;
    PROCESS_INFORMATION pi;
    pclient client;
 
+  // in the case of usestdin, the last argument is in fact not passed to
+  // CreateProcess, it contains the filename instead
+   if (r->usestdin) {
+     argcount--;
+   }
+
    client = (pclient) list_lookup(clients, r->key);
    if (client==NULL) {
       return;
@@ -246,6 +253,17 @@ void run_request (prequest r) {
    // set the stdout for the childprocess
    si.hStdOutput = outfilehandle;
    si.hStdError = outfilehandle;
+   if (r->usestdin) {
+     infilehandle =
+       CreateFile(r->args[argcount],
+                 GENERIC_READ,
+                 FILE_SHARE_READ,
+                 NULL,
+                 OPEN_ALWAYS,
+                 FILE_ATTRIBUTE_NORMAL,
+                 NULL);
+     si->hSdtInput = infilehandle;
+   }
    // if we don't set that flag, the stdout we just set won't even be looked at
    si.dwFlags = STARTF_USESTDHANDLES;
    /* Compute command line string. When a parameter contains a " or a space we
@@ -260,7 +278,7 @@ void run_request (prequest r) {
    /* Now take care of the arguments */
    {
      int k;
-     for (k = 0; k < r->numargs; k++)
+     for (k = 0; k < argcount; k++)
        {
          char *ca = r->args[k]; /* current arg */
          int ca_index; /* index of the current character in ca */