Updated web page

SMTInterpol/web/html/index.xml

@@ -35,17 +35,20 @@
 
     <head1>Team</head1>
     <txt><s /> is developed by <link
-    url="http://swt.informatik.uni-freiburg.de/staff/christ">J&uuml;rgen
-    Christ</link>, <link
     url="http://swt.informatik.uni-freiburg.de/staff/hoenicke">Jochen
-    Hoenicke</link>, <link
-    url="http://swt.informatik.uni-freiburg.de/staff/nutz">Alexander
-    Nutz</link>, and <link
+    Hoenicke</link> and <link
     url="http://swt.informatik.uni-freiburg.de/staff/schindler">Tanja
-    Schindler</link> in the context of the <link
-    url="http://www.avacs.org">AVACS (Automatic Verification and Analysis of
-    Complex Systems)</link> project.  If you have any questions, suggestions,
-    or if you want to contribute, feel free to contact us.</txt>
+    Schindler</link> in the context of the SIGSMCAP
+    (SMT-based Interpolant Generation
+    for Software ModelChecking of Array Programs) project and
+    Alexander Nutz.
+    If you have any questions, suggestions,
+    or if you want to contribute, feel free to contact us.
+    Previous contributors include
+    J&uuml;rgen Christ.</txt>
+
+    <head1>Bug Reports</head1>
+    <txt>Please use our <link url="https://github.com/ultimate-pa/smtinterpol/issues">github page</link> to report bugs.</txt>
 
     <head1>License</head1>
     <txt><s /> is distributed under LGPL Version 3.</txt>
@@ -54,13 +57,5 @@
     <txt><s /> participates regularly in the <link
     url="http://smtcomp.sourceforge.net">SMT-COMP</link>. See this page or
     the news page for further details.</txt>
-
-    <head1>Further Development</head1>
-    <txt>We plan to extend <s /> to reason
-    about arrays and quantifiers.  Interpolation procedures for these
-    logics will be the next big challenge.  Additionally, we try to add
-    more flexibility to our interpolation engine to enable model checkers
-    to easily adjust the interpolation procedure
-    of <s /> to their needs.</txt>
   </content>
 </page>

SMTInterpol/web/html/news.xml

@@ -9,6 +9,15 @@
 <page id="news">
   <name>News</name>
   <content>
+    <head1>New release 2.5</head1>
+    <txt>We released version 2.5 of <s />.
+    This release has full support for the quantifier free fragment for
+    arrays.  Although this theory have been supported in the solver for a
+    while, the new release also supports generation of interpolants for
+    this theory.
+    We also updated the parser to support SMTLIB version 2.5.
+    </txt>
+
     <head1><s /> at SMTCOMP 2014</head1>
     <txt>We participated in the SMTCOMP 2014 which was part of the Vienna Summer of Logic Olympic Games.  The primary new feature was our array solver which performed really good.  We were awarded with the  G&ouml;del medal for the second place according to the multi-division error-free scoring.  Furthermore, David Cok - the lead organizer of the competition - awarded us with a beautiful "big A" also known as a universal quantifier when put in correct position.  We thank all the supporters that helped to improve <s /> and, of course, the organizers of the competition and the VSL olympic games for these nice awards.<br /><img src="floc2014.jpg" alt="Awards for SMTInterpol during VSL 2014" /><img src="goedel.jpg" alt="The goedel medal" /></txt>