diff --git a/gui/Scyther/Bin/scyther-linux b/gui/Scyther/Bin/scyther-linux
index 7e7905a..3c682e1 100755
Binary files a/gui/Scyther/Bin/scyther-linux and b/gui/Scyther/Bin/scyther-linux differ
diff --git a/gui/Scyther/Bin/scyther-w32.exe b/gui/Scyther/Bin/scyther-w32.exe
index ced9599..9092afc 100755
Binary files a/gui/Scyther/Bin/scyther-w32.exe and b/gui/Scyther/Bin/scyther-w32.exe differ
diff --git a/gui/Scyther/Scyther.py b/gui/Scyther/Scyther.py
index d81f8cb..ca5b812 100755
--- a/gui/Scyther/Scyther.py
+++ b/gui/Scyther/Scyther.py
@@ -125,6 +125,7 @@ class Scyther(object):
         self.errorcount = 0
         self.run = False
         self.output = None
+        self.cmd = None
 
         # defaults
         self.xml = True     # this results in a claim end, otherwise we simply get the output
@@ -150,6 +151,10 @@ class Scyther(object):
             self.spdl += l
         fp.close()
 
+    def addArglist(self,arglist):
+        for arg in arglist:
+            self.options += " %s" % (arg)
+
     def doScytherCommand(self, spdl, args):
         """ 
         Run Scyther backend on the input
@@ -169,28 +174,31 @@ class Scyther(object):
         # Sanitize input somewhat
         if not spdl or spdl == "":
             # Scyther hickups on completely empty input
-            spdl = " "
+            spdl = None
 
         # Generate temporary files for the output
         # Requires Python 2.3 though.
         (fde,fne) = tempfile.mkstemp()  # errors
         (fdo,fno) = tempfile.mkstemp()  # output
-        (fdi,fni) = tempfile.mkstemp()  # input
+        if spdl:
+            (fdi,fni) = tempfile.mkstemp()  # input
 
-        # Write (input) file
-        fhi = os.fdopen(fdi,'w+b')
-        fhi.write(spdl)
-        fhi.close()
+            # Write (input) file
+            fhi = os.fdopen(fdi,'w+b')
+            fhi.write(spdl)
+            fhi.close()
 
         # Generate command line for the Scyther process
         self.cmd = ""
         self.cmd += "\"%s\"" % self.program
         self.cmd += " --append-errors=%s" % fne
         self.cmd += " --append-output=%s" % fno
-        self.cmd += " %s %s" % (self.options, args)
+        self.cmd += " %s" % args
         if spdl:
             self.cmd += " %s" % fni
 
+        print self.cmd
+
         # Start the process
         os.system(self.cmd)
 
@@ -205,7 +213,8 @@ class Scyther(object):
         fho.close()
         os.remove(fne)
         os.remove(fno)
-        os.remove(fni)
+        if spdl:
+            os.remove(fni)
 
         return (output,errors)
 
diff --git a/gui/Scyther/XMLReader.py b/gui/Scyther/XMLReader.py
index e8bf410..4bb8eda 100644
--- a/gui/Scyther/XMLReader.py
+++ b/gui/Scyther/XMLReader.py
@@ -179,6 +179,22 @@ class XMLReader(object):
             action = self.readEvent(eventxml)
             action.run = run
             run.eventList.append(action)
+        for variable in xml.find('variables'):
+            # Read the variables one by one
+            assert(variable.tag == 'variable')
+            var = self.readTerm(variable.find('name').find('term'))
+            var.types = self.readTypeList(variable.find('name'))
+            
+            substxml = variable.find('substitution')
+            # Read substitution if present
+            if substxml != None:
+                subst = self.readTerm(substxml.find('term'))
+                subst.types = self.readTypeList(substxml)
+                newvar = Term.TermVariable(var.name,subst)
+                newvar.types = var.types
+                var = newvar
+
+            run.variables.append(var)
         return run
             
     # Read protocol description for a certain role
diff --git a/src/xmlout.c b/src/xmlout.c
index 875575c..48ebe51 100644
--- a/src/xmlout.c
+++ b/src/xmlout.c
@@ -395,6 +395,34 @@ xmlVariable (const System sys, const Term variable, const int run)
     }
 }
 
+//! Show variable instantiations
+/**
+ * Show the instantiations of all variables. Maybe we need to restrict this,
+ * and scan only for those variables that actually occur in the semitrace.
+ */
+void
+xmlRunVariables (const System sys, const int run)
+{
+  int prev_mode;		// buffer for show mode
+  Termlist varlist;
+
+  prev_mode = show_substitution_path;
+  show_substitution_path = true;
+  xmlPrint ("<variables>");
+  xmlindent++;
+
+  varlist = sys->runs[run].sigma;
+  while (varlist != NULL)
+    {
+      xmlVariable (sys, varlist->term, run);
+      varlist = varlist->next;
+    }
+
+  xmlindent--;
+  xmlPrint ("</variables>");
+  show_substitution_path = prev_mode;
+}
+
 //! Show variable instantiations
 /**
  * Show the instantiations of all variables. Maybe we need to restrict this,
@@ -813,6 +841,7 @@ xmlRunInfo (const System sys, const int run)
       xmlOutTerm ("agent", r->nameterm);
     }
   xmlAgentsOfRunPrint (sys, run);
+  xmlRunVariables (sys, run);
 }
 
 //! Display runs