mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

fixed bug detected in regression tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-07 10:46:00 -08:00
parent c5b91aef68
commit 73a13f209b
2 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/ast.cpp
View file

@ -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++)

2
src/ast/ast.h
View file

@ -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); }