Skip to content

Commit 1ef6941

Browse files
committed
Termination: Parse 0-ary locations correctly
Previously, we assumed that all terms are given as tuples. However, we should allow 0-ary terms to be just atoms, instead of 1-tuples.
1 parent b4bbf06 commit 1ef6941

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

src/termination/Frontend.cc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,8 @@ LocationDeclaration ITS::parseFun(SExpression const & expr) {
262262
}
263263

264264
Location ITS::parseLocationInstance(SExpression const & expr) {
265+
if (isAtom(expr)) return {asAtom(expr), {}};
266+
265267
auto const & args = asSubExpressions(expr);
266268
if (args.empty()) throw std::runtime_error("Location instance cannot be empty");
267269

0 commit comments

Comments
 (0)