diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m index 7d03c65f6d55cbb42abe2f6cd17778428c56b538..90cf8f6a06c642028c77d1f17d13a49b3044b82d 100644 --- a/@CVC_checker/cvc_check.m +++ b/@CVC_checker/cvc_check.m @@ -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 = [];