generate existential vars to handle reuse optimizationDiscussion w Xavier: replace this mechanism (fragile because of non-constructive witnesses) with a ghost-variables-based mechanism
generate existential vars to handle reuse optimization
Discussion w Xavier: replace this mechanism (fragile because of non-constructive witnesses) with a ghost-variables-based mechanism