ultimate icon indicating copy to clipboard operation
ultimate copied to clipboard

Published 20 hours ago • verified publisher icon ultimate-pa

Support Skolem functions in TreeAutomizer

Open maul-esel opened this issue 5 months ago • 0 comments

As observed in #676, TreeAutomizer does not support Horn clauses with Skolem functions, which our frontend introduces for existentially-quantified variables.

We need to figure out how to treat Skolem functions in the feasibility check (TreeChecker or HCSSABuilder).

maul-esel avatar Sep 24 '24 19:09 maul-esel