From b12a1caa0759052380d60fbd1f71a5d8436ac047 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Mar 2018 09:05:44 -0700
Subject: [PATCH] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_str.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 30092097a..e1340c301 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -321,7 +321,7 @@ namespace smt {
             T_cut * varInfo = alloc(T_cut);
             m_cut_allocs.push_back(varInfo);
             varInfo->level = slevel;
-            varInfo->vars[node] = 1;
+            varInfo->vars.insert(node, 1);
             cut_var_map.insert(baseNode, std::stack<T_cut*>());
             cut_var_map[baseNode].push(varInfo);
             TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
@@ -330,7 +330,7 @@ namespace smt {
                 T_cut * varInfo = alloc(T_cut);
                 m_cut_allocs.push_back(varInfo);
                 varInfo->level = slevel;
-                varInfo->vars[node] = 1;
+                varInfo->vars.insert(node, 1);
                 cut_var_map[baseNode].push(varInfo);
                 TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
             } else {
@@ -339,11 +339,11 @@ namespace smt {
                     m_cut_allocs.push_back(varInfo);
                     varInfo->level = slevel;
                     cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
-                    varInfo->vars[node] = 1;
+                    varInfo->vars.insert(node, 1);
                     cut_var_map[baseNode].push(varInfo);
                     TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
                 } else if (cut_var_map[baseNode].top()->level == slevel) {
-                    cut_var_map[baseNode].top()->vars[node] = 1;
+                    cut_var_map[baseNode].top()->vars.insert(node, 1);
                     TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
                 } else {
                     get_manager().raise_exception("entered illegal state during add_cut_info_one_node()");