Open c-cube opened 8 years ago
call CVC4 with --fmf-empty-sorts to avoid refining recursive functions that are not used. We need to force it to fill other sorts though, by declaring p : sort -> bool, c : sort, and p(c) if we want to ensure that sort is not empty.
--fmf-empty-sorts
p : sort -> bool
c : sort
p(c)
sort
call CVC4 with
--fmf-empty-sortsto avoid refining recursive functions that are not used. We need to force it to fill other sorts though, by declaringp : sort -> bool,c : sort, andp(c)if we want to ensure thatsortis not empty.