summaryrefslogtreecommitdiff
path: root/src/compat/cvc3_compat.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r--src/compat/cvc3_compat.cpp2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 0cd35ce0d..9fbdeb8d0 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1261,6 +1261,7 @@ Type ValidityChecker::createType(const std::string& typeName) {
Type ValidityChecker::createType(const std::string& typeName, const Type& def) {
d_parserContext->defineType(typeName, def);
+ return def;
}
Type ValidityChecker::lookupType(const std::string& typeName) {
@@ -1279,6 +1280,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type,
const Expr& def) {
CVC4::CheckArgument(def.getType() == type, def, "expected types to match");
d_parserContext->defineVar(name, def);
+ return def;
}
Expr ValidityChecker::lookupVar(const std::string& name, Type* type) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback