diff -r 0faeabd99289 -r 0ea45a4d32f3 src/HOL/SMT/lib/scripts/remote_smt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/lib/scripts/remote_smt	Mon Feb 08 11:01:47 2010 +0100
@@ -0,0 +1,31 @@
+#!/usr/bin/env perl
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# Invoke remote SMT solvers.
+
+use strict;
+use warnings;
+use LWP;
+
+
+# arguments
+
+my $solver = $ARGV[0];
+my @options = @ARGV[1 .. ($#ARGV - 1)];
+my $problem_file = $ARGV[-1];
+
+
+# call solver
+
+my $agent = LWP::UserAgent->new;
+$agent->agent("SMT-Request");
+$agent->timeout(180);
+my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
+  "Solver" => $solver,
+  "Options" => join(" ", @options),
+  "Problem" => [$problem_file] ],
+  "Content_Type" => "form-data");
+if (not $response->is_success) { die "HTTP-Error: " . $response->message; }
+else { print $response->content; }
+