diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
| commit | 9de66957df6448ba1243cdb7cc84813fe82e69d5 (patch) | |
| tree | 9c013455d7f0c0e057f44f51abdead7ff1ebd01c /src/theory/builtin/kinds | |
| parent | 23367b1eac54a17a060697b1cf187ad2cc2ff503 (diff) | |
fix get-value output in a couple ways; this fixes bug #378
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index e52196163..285eb651f 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -295,7 +295,7 @@ operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" variable SKOLEM "skolem var" variable VARIABLE "variable" -operator TUPLE 2: "a tuple" +operator TUPLE 1: "a tuple" constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ @@ -307,7 +307,7 @@ cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" well-founded FUNCTION_TYPE false -operator TUPLE_TYPE 2: "tuple type" +operator TUPLE_TYPE 1: "tuple type" cardinality TUPLE_TYPE \ "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" |