summaryrefslogtreecommitdiff
path: root/src/theory/builtin/kinds
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-09 09:49:35 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-09 09:49:35 +0000
commit0131e18b811bdf2825a1cde5a6d68d523b19aacc (patch)
tree9c4dcb4c1bf355b943926a5df85d3c3446750878 /src/theory/builtin/kinds
parentec86769172d29ff7f5ed959866ecef339264552b (diff)
support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss
Diffstat (limited to 'src/theory/builtin/kinds')
-rw-r--r--src/theory/builtin/kinds2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 47ee8cbfc..ad442fc2f 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -119,7 +119,7 @@ constant BUILTIN \
"The kind of nodes representing built-in operators"
variable FUNCTION "function"
-parameterized APPLY FUNCTION 1: "defined function application"
+parameterized APPLY FUNCTION 0: "defined function application"
operator EQUAL 2 "equality"
operator DISTINCT 2: "disequality"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback