summaryrefslogtreecommitdiff
path: root/src/parser/cvc/cvc_parser.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc/cvc_parser.g')
-rw-r--r--src/parser/cvc/cvc_parser.g2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 55ae0ff73..acf0394d0 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -323,7 +323,7 @@ term returns [CVC4::Expr t]
LPAREN formulaList[args] RPAREN
// TODO: check arity
- { t = mkExpr(CVC4::kind::APPLY, args); }
+ { t = mkExpr(CVC4::kind::APPLY_UF, args); }
| /* if-then-else */
t = iteTerm
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback