Solves some issues with variables reported by CHCs:
does not provide sorts for input and output variables i and o. These are derivable from the CHC’s head signature, so not a big deal
does not provide which symbol is the term variable t0.
does not list auxiliary variables (e.g., y) separately. There is a single “variables” property with input, output, and auxiliary variables. ****This allows an ambiguity when the same symbol is both an input/output variable**** and ****shadowed as an auxiliary variable****.
$\forall i, o.\; X.Sem(t, i, o) \impliedby \exists i.\; ChcBody(i, o)$
Solves some issues with variables reported by CHCs:
i
ando
. These are derivable from the CHC’s head signature, so not a big dealt0
.y
) separately. There is a single “variables” property with input, output, and auxiliary variables. ****This allows an ambiguity when the same symbol is both an input/output variable**** and ****shadowed as an auxiliary variable****.