From 3e810d6c547e404cbc96aea0972485434d0baecd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 5 Feb 2018 16:46:49 -0800
Subject: [PATCH] remove static from format (not thread safe), remove std::move
 #1466

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/format.cpp             | 4 ++--
 src/ast/proofs/proof_utils.h   | 2 +-
 src/muz/rel/dl_instruction.cpp | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/ast/format.cpp b/src/ast/format.cpp
index 835892121..6c2a02989 100644
--- a/src/ast/format.cpp
+++ b/src/ast/format.cpp
@@ -151,7 +151,7 @@ namespace format_ns {
     }
     
     format * mk_int(ast_manager & m, int i) {
-        static char buffer[128];
+        char buffer[128];
 #ifdef _WINDOWS
         sprintf_s(buffer, ARRAYSIZE(buffer), "%d", i);
 #else
@@ -161,7 +161,7 @@ namespace format_ns {
     }
     
     format * mk_unsigned(ast_manager & m, unsigned u) {
-        static char buffer[128];
+        char buffer[128];
 #ifdef _WINDOWS
         sprintf_s(buffer, ARRAYSIZE(buffer), "%u", u);
 #else
diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index 473df31e6..455f39c4f 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -88,7 +88,7 @@ class elim_aux_assertions {
 
     app_ref m_aux;
 public:
-    elim_aux_assertions(app_ref aux) : m_aux(std::move(aux)) {}
+    elim_aux_assertions(app_ref const& aux) : m_aux(aux) {}
 
     void mk_or_core(expr_ref_vector &args, expr_ref &res)
     {
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 0a33e99f1..26139fb7c 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -190,8 +190,8 @@ namespace datalog {
         func_decl_ref m_pred;
         reg_idx m_reg;
     public:
-        instr_io(bool store, func_decl_ref pred, reg_idx reg)
-            : m_store(store), m_pred(std::move(pred)), m_reg(reg) {}
+        instr_io(bool store, func_decl_ref const& pred, reg_idx reg)
+            : m_store(store), m_pred(pred), m_reg(reg) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
             if (m_store) {