diff --git a/@PVS_checker/parse_pvs_result.m b/@PVS_checker/parse_pvs_result.m
index 817adb769cf7c171654004ffa4487aeef81f48ad..bec651b4f34eed62ed0cb6645b24ec35cd43c4ad 100644
--- a/@PVS_checker/parse_pvs_result.m
+++ b/@PVS_checker/parse_pvs_result.m
@@ -24,12 +24,12 @@ else
             % These parsing depend on the version of PVS used,
             % which may be a bad idea, although pvs is not
             
-            if strncmp(object.pvs_version,'PVS Version 4.0',15)
+            if object.pvs_version <= 4.0
                 % 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)
+            elseif object.pvs_version <= 4.2
                 search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
-            elseif strncmp(object.pvs_version,'PVS Version ',12) && str2num(object.pvs_version(13:15))>=5.0
+            elseif object.pvs_version >= 5.0
                 search_str =  sprintf('(?<=Installing rewrite rule.*\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
             end
             found2 = regexp(result,char(search_str),'match','once');
diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m
index aa2b7b8d9fa273a41e6e7cef640649dd31508498..17d221d61c877d6661e02e1e0ead190acf72a20b 100644
--- a/@PVS_checker/pvs_check.m
+++ b/@PVS_checker/pvs_check.m
@@ -31,7 +31,9 @@ end
 
 
 
-object.pvs_version = PVS_checker.get_pvs_version;
+version_string = PVS_checker.get_pvs_version;
+version = regexp(version_string, 'PVS Version (...)', 'tokens');
+object.pvs_version = str2double(char(version{1}));
 
 
 % THIS SECTION NEEDS SOME WORK