From ee410adc01be424c3e5e28f273153afd66a49a83 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 25 May 2012 16:05:23 -0700
Subject: [PATCH] nodestack: bugfix - fixup allocators for vectors

---
 nodestack.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/nodestack.h b/nodestack.h
index bd64c4a..eebfa5b 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -35,8 +35,8 @@ private:
 	static int total_nodes;
 	ModelAction *action;
 	int num_threads;
-	std::vector<bool> explored_children;
-	std::vector<bool> backtrack;
+	std::vector< bool, MyAlloc<bool> > explored_children;
+	std::vector< bool, MyAlloc<bool> > backtrack;
 };
 
 typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
-- 
2.34.1