diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m
index 8dc62b8b46d5d770b6b51522dbe2912f04eee48f..55472cc574e5ff2e2647c7ba8002fe028ce692b8 100644
--- a/@CVC_checker/cvc_check.m
+++ b/@CVC_checker/cvc_check.m
@@ -19,10 +19,10 @@ function [ check, seqs ] = cvc_check( object )
 [filename, queries] = object.generate_file;
 
     waitbar(.10,box,'Running Proof');
-
+tic
     % run the cvc command
-[status, result] = system(['cvc3 ' filename ' +model'])
-
+[status, result] = system(['cvc3 ' filename ' +model']);
+toc
 % check return status for errors
 if (status ~= 0)
     
diff --git a/@PVS_checker/generate_pvs_file.m b/@PVS_checker/generate_pvs_file.m
index 4434e4b6a9473f7de013008107e064d1092f4e8a..ddfbba5ef9c9d2f2f7851e322e6233d62b0e4815 100644
--- a/@PVS_checker/generate_pvs_file.m
+++ b/@PVS_checker/generate_pvs_file.m
@@ -130,23 +130,7 @@ end
     end
     code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];
     
-%else
-    %inputs_new = [];
-    %for i=1:size(object.input_type,1)
-        
-        
-    %    inputs_new = [inputs_new char(object.input_type(i,1)) ':' PVS_checker.matlab_type_to_pvs_type(char(object.input_type(i,2)))];
-        
-    %    if(i~=(size(object.input_type,1)))
-    %            inputs_new = [inputs_new ','];
-    %    end
-    %end
-    %code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];
-    
-    %code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)];
-    
-    
-%end
+
 code = [code object.generate_pvs(object.data.Grid1,object.data.Grid2,0)];
 code = [code sprintf('\nEND %s',function_name)];
 fprintf(fileid,code);
diff --git a/@PVS_checker/generate_pvs_script.m b/@PVS_checker/generate_pvs_script.m
index 83d277aac84109d6ca4708648684cb5345e09c22..589689d083598b0fbdee5319d586bad81a15a79d 100644
--- a/@PVS_checker/generate_pvs_script.m
+++ b/@PVS_checker/generate_pvs_script.m
@@ -9,10 +9,13 @@
 %    none
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
-function [] = generate_pvs_script(object,filename)
+function [] = generate_pvs_script(object,filename,sim_types)
 fileid = fopen([filename '.el'],'w');
-code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];
-
+%if sim_types == 0 
+code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];
+%else
+%    code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];
+%end
 fprintf(fileid,code);
 fclose(fileid);
 end
diff --git a/@PVS_checker/parse_pvs_result.m b/@PVS_checker/parse_pvs_result.m
index 2ef3994e3eefe1f78b5f348ae4297a3a49fe7724..c851be194cefc207bf5684864709834ff8d0f754 100644
--- a/@PVS_checker/parse_pvs_result.m
+++ b/@PVS_checker/parse_pvs_result.m
@@ -28,10 +28,10 @@ else
                 % 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)
-                search_str =  sprintf('(?<=Installing rewrite rule singleton_rew\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
+                search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
             end
             found2 = regexp(result,char(search_str),'match','once');
-            
+          
             
             % find the counter examples
             search_str = sprintf('(?<=%s.*?substitutions:).*?(?=This will undo the proof to: \\n%s)|(?<=%s.*?)No counter-examples(?=.*?%s)',char(found(i)),char(found(i)),char(found(i)),char(found(i)));
diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m
index f0aff8a3c1487dfb51cd51025edcc5e61c4b8708..7852872e26422b6c145842eb3f70cf80a2140273 100644
--- a/@PVS_checker/pvs_check.m
+++ b/@PVS_checker/pvs_check.m
@@ -52,12 +52,14 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove'))
     
     
     % generate the proof script
-    object.generate_pvs_script(function_name);
+    object.generate_pvs_script(function_name,1);
     waitbar(.10,box,'Running Proof');
     %---------
     % call pvs in batch mode with script
     % ADD check that pvs actually exists in system
+    tic
     [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el'])
+    toc
     %objectect.msgbox_scroll(result);
     waitbar(.70,box,'Parsing Results');
     [parsed error] = object.parse_pvs_result(result);
@@ -76,7 +78,7 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove'))
     end
     waitbar(.100,box,'Deleting Proof Script');
     
-    delete([function_name '.el']);
+    %delete([function_name '.el']);
     
     delete(box);
 end
diff --git a/@PVS_checker/pvs_check_for_imports.m b/@PVS_checker/pvs_check_for_imports.m
index e5e2c3a468ee9d8e1dd871c1afac6ac157a35a9d..6e9e5c534868eaaed05b29848d9cd770c91063b6 100644
--- a/@PVS_checker/pvs_check_for_imports.m
+++ b/@PVS_checker/pvs_check_for_imports.m
@@ -22,7 +22,8 @@ function string = pvs_check_for_imports(object)
 
 hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'}};
 for k=1:size(hashtable,2)
-    functions = regexp(object.data.function_inputs,hashtable{k}(1),'once')
+    
+    functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once')
             if ~isempty(functions{1})
                 if (~any(ismember(found,hashtable{k}(1))))
                 string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];