summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-10-28 14:51:41 -0500
committerGitHub <noreply@github.com>2020-10-28 14:51:41 -0500
commit3ed42d7aba07db5801cf8245890035192aa06b15 (patch)
tree83299050be1fa63e14acf55455032f0763372b63 /src/api/cvc4cpp.cpp
parenta61f77fd58c8da0f38de4d094258f78f71774383 (diff)
Convert symbol table from Expr-level to Term-level (#5355)
This task is left over from parser migration. This PR also drops support for a case of symbol overloading, in particular symbols (constructors, selectors) for parametric datatypes cannot be overloaded. One regression is disabled as a result.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r--src/api/cvc4cpp.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 3cfeaf6cd..e198c0d89 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2082,7 +2082,7 @@ std::ostream& operator<<(
size_t TermHashFunction::operator()(const Term& t) const
{
- return ExprHashFunction()(t.d_node->toExpr());
+ return NodeHashFunction()(*t.d_node);
}
/* -------------------------------------------------------------------------- */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback