Commits

Leonardo de Moura committed 73a13f2

fixed bug detected in regression tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

  • Participants
  • Parent commits c5b91ae

Comments (0)

Files changed (2)

File src/ast/ast.cpp

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

File src/ast/ast.h

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