From 4359d518a9cfa5298bd81107f9d0ad24651c7e5c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Jul 2018 09:28:22 -0700
Subject: [PATCH] thanks Nuno

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp | 5 -----
 src/ast/ast.h   | 6 +++++-
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index ce3cad403..ac7ce156d 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1371,11 +1371,6 @@ void ast_manager::update_fresh_id(ast_manager const& m) {
     m_fresh_id = std::max(m_fresh_id, m.m_fresh_id);
 }
 
-void ast_manager::inc_ref(ast * n) {
-    if (n) {
-        n->inc_ref();
-    }
-}
 
 void ast_manager::init() {
     m_int_real_coercions = true;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index c4efe4ad3..aa8669def 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1622,7 +1622,11 @@ public:
 
     void debug_ref_count() { m_debug_ref_count = true; }
 
-    void inc_ref(ast * n);
+    void inc_ref(ast * n) {
+        if (n) {
+            n->inc_ref();
+        }
+    }
     
     void dec_ref(ast* n) {
         if (n) {