From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 2 Aug 2020 12:57:24 +0000 (-0700)
Subject: Fix ASan failure in interactive_shell_black (#4827)
X-Git-Tag: cvc5-1.0.0~3057
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76b25e75c198f9af7ba2c2554e07fec5ba047597;p=cvc5.git

Fix ASan failure in interactive_shell_black (#4827)

This commit fixes an issue reported by ASan for unit test
interactive_shell_black. The unit test was failing because nodes were
created in the wrong node manager. The issue was likely introduced with
e8bbee7.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 1c15466a1..61d180fe4 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1414,13 +1414,19 @@ size_t OpHashFunction::operator()(const Op& t) const
 Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
 
 Term::Term(const Solver* slv, const CVC4::Expr& e)
-    : d_solver(slv), d_node(new CVC4::Node(e))
+    : d_solver(slv)
 {
+  // Ensure that we create the node in the correct node manager.
+  NodeManagerScope scope(d_solver->getNodeManager());
+  d_node.reset(new CVC4::Node(e));
 }
 
 Term::Term(const Solver* slv, const CVC4::Node& n)
-    : d_solver(slv), d_node(new CVC4::Node(n))
+    : d_solver(slv)
 {
+  // Ensure that we create the node in the correct node manager.
+  NodeManagerScope scope(d_solver->getNodeManager());
+  d_node.reset(new CVC4::Node(n));
 }
 
 Term::~Term()