From 73a13f209bcdc28782c000e5504445923e9b098e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Nov 2012 10:46:00 -0800 Subject: [PATCH] fixed bug detected in regression tests Signed-off-by: Leonardo de Moura --- src/ast/ast.cpp | 7 +++++++ src/ast/ast.h | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 64df1d830..6763d1d55 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2219,6 +2219,13 @@ app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args) // // ----------------------------------- +expr_dependency * ast_manager::mk_leaf(expr * t) { + if (t == 0) + return 0; + else + return m_expr_dependency_manager.mk_leaf(t); +} + expr_dependency * ast_manager::mk_join(unsigned n, expr * const * ts) { expr_dependency * d = 0; for (unsigned i = 0; i < n; i++) diff --git a/src/ast/ast.h b/src/ast/ast.h index 17b4d2dac..8453598f2 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1777,7 +1777,7 @@ public: // ----------------------------------- public: expr_dependency * mk_empty_dependencies() { return m_expr_dependency_manager.mk_empty(); } - expr_dependency * mk_leaf(expr * t) { return m_expr_dependency_manager.mk_leaf(t); } + expr_dependency * mk_leaf(expr * t); expr_dependency * mk_join(unsigned n, expr * const * ts); expr_dependency * mk_join(expr_dependency * d1, expr_dependency * d2) { return m_expr_dependency_manager.mk_join(d1, d2); } void inc_ref(expr_dependency * d) { if (d) m_expr_dependency_manager.inc_ref(d); }