summaryrefslogtreecommitdiff
path: root/src/compat/cvc3_compat.cpp
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-03-27 14:07:59 -0400
committerlianah <lianahady@gmail.com>2013-03-27 14:07:59 -0400
commit2109b16d2b38bba633fb54d5f9c62fecab8d771b (patch)
treea474276db492ce41753a8201498b5832b35dd300 /src/compat/cvc3_compat.cpp
parentcab30c6cac6921efc19fcc11b0cf5afa7770cb5b (diff)
parentad5e31e2031349c9b9d0bf5d9fcaa1ea7950db58 (diff)
Merge branch 'master' into bv-core
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