If we try to analyze problems such as HWV067+1.p, Serkr immediately crashes due to a stack overflow. This is not really surprising though, since the problem has 35000 nested quantifiers. The fix for this is to simply modify the AST so that a single quantifier can bind multiple variables instead of just one.
If we try to analyze problems such as HWV067+1.p, Serkr immediately crashes due to a stack overflow. This is not really surprising though, since the problem has 35000 nested quantifiers. The fix for this is to simply modify the AST so that a single quantifier can bind multiple variables instead of just one.