diff --git a/@PVS_checker/parse_pvs_result.m b/@PVS_checker/parse_pvs_result.m
index 1794ead1cd3d090a8147bf5f231542c8320f4bd9..3f552b46af50d2212495cf2958ecdf4ae37727db 100644
--- a/@PVS_checker/parse_pvs_result.m
+++ b/@PVS_checker/parse_pvs_result.m
@@ -5,8 +5,8 @@
 %   object:PVS_checker - PVS_checker object
 %   result:string - string containing text that comes back from pvs
 % outputs:
-%   output:structure - results paresed into structure for easier
-%       manipulatings
+%   output:structure - results parsed into structure for easier
+%       manipulating
 %   error:boolean - 0 if no error, 1 if error found during parsing.
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
@@ -27,8 +27,10 @@ else
             if strncmp(object.pvs_version,'PVS Version 4.0',15)
                 % find the TCC that was unprovable
                 search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)));
-            elseif strncmp(object.pvs_version,'PVS Version 4.2',15) || strncmp(object.pvs_version,'PVS Version 5.0',15)
+            elseif strncmp(object.pvs_version,'PVS Version 4.2',15)
                 search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
+            elseif strncmp(object.pvs_version,'PVS Version 5.0',15)
+                search_str =  sprintf('(?<=Installing rewrite rule.*\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
             end
             found2 = regexp(result,char(search_str),'match','once');