diff options
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index afac925e2..62885f55f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -330,7 +330,7 @@ bool Expr::isString() const { } bool Expr::isBoundVar() const { - Unimplemented(); + return getKind() == CVC4::kind::BOUND_VARIABLE; } bool Expr::isLambda() const { @@ -1857,7 +1857,7 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid, const Type& type) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + return d_em->mkBoundVar(name, type); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) { |