Commit 0dd1d306 authored by Colin Eles's avatar Colin Eles
Browse files

now gives proper error if cvc sees theory is incomplete, ie. if there are non-linear formulas.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6524 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 2d32176d
Loading
Loading
Loading
Loading
+16 −0
Original line number Diff line number Diff line
@@ -25,6 +25,22 @@ end
    waitbar(.70,box,'Parsing Results');

seqs = [];

% look for incompleteness, happens with non-linear artihmetic, ie.
% multiplication
incomplete = regexp(result,'CVC3 was incomplete in this example due to','match');
if ~isempty(incomplete)
    incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once')
    msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]);
    
        check = 0;
        seqs = 'canceled';
        delete(box);
        return;
    
end


for i = 1:size(queries,2)
    asserts = [];