From 5e4d1151ebd90c4c9556a79e38af025682292df9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 5 Dec 2012 15:20:16 -0800
Subject: [PATCH] fixing clang compilation problems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/muz_qe/qe_sat_tactic.cpp      | 4 ++--
 src/smt/expr_context_simplifier.h | 2 +-
 src/util/cooperate.cpp            | 2 +-
 src/util/memory_manager.cpp       | 1 +
 src/util/scoped_timer.cpp         | 1 +
 src/util/timeout.cpp              | 1 +
 6 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp
index f33de6382..854e15493 100644
--- a/src/muz_qe/qe_sat_tactic.cpp
+++ b/src/muz_qe/qe_sat_tactic.cpp
@@ -629,7 +629,7 @@ namespace qe {
             expr_ref fml(_fml, m);
             if (m_strong_context_simplify_param && m_ctx_simplify_local_param) {
                 m_ctx_rewriter.push();
-                m_ctx_rewriter.assert(M(idx));
+                m_ctx_rewriter.assert_expr(M(idx));
                 m_ctx_rewriter(fml);
                 m_ctx_rewriter.pop();
                 TRACE("qe", tout << mk_pp(_fml, m) << "\n-- context simplify -->\n" << mk_pp(fml, m) << "\n";);
@@ -650,7 +650,7 @@ namespace qe {
             m_rewriter(not_fml);
             if (m_strong_context_simplify_param && !m_ctx_simplify_local_param) {
                 m_ctx_rewriter.push();
-                m_ctx_rewriter.assert(M(idx));
+                m_ctx_rewriter.assert_expr(M(idx));
                 m_ctx_rewriter(not_fml);
                 m_ctx_rewriter.pop();
             }
diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h
index 2c1f32ddc..982b65878 100644
--- a/src/smt/expr_context_simplifier.h
+++ b/src/smt/expr_context_simplifier.h
@@ -75,7 +75,7 @@ public:
     void operator()(expr_ref& result) { simplify(result.get(), result); }
     void push() { m_solver.push(); }
     void pop() { m_solver.pop(1); }
-    void assert(expr* e) { m_solver.assert_expr(e); }
+    void assert_expr(expr* e) { m_solver.assert_expr(e); }
     
     void collect_statistics(statistics & st) const { m_solver.collect_statistics(st); }
     void reset_statistics() { m_solver.reset_statistics(); }
diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp
index c941b18e5..cdd91bfdd 100644
--- a/src/util/cooperate.cpp
+++ b/src/util/cooperate.cpp
@@ -16,10 +16,10 @@ Author:
 Notes:
 
 --*/
-#include"z3_omp.h"
 #include"cooperate.h"
 #include"trace.h"
 #include"debug.h"
+#include"z3_omp.h"
 
 struct cooperation_lock {
     omp_nest_lock_t  m_lock;
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index be08fe50f..de4e760d7 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -4,6 +4,7 @@
 #include"trace.h"
 #include"memory_manager.h"
 #include"error_codes.h"
+#include"z3_omp.h"
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
 // For example, rational.h contains
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 5f9d554f9..4b191505f 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -58,6 +58,7 @@ Revision History:
 #endif
 #include"util.h"
 #include<limits.h>
+#include"z3_omp.h"
 
 struct scoped_timer::imp {
     event_handler *  m_eh;
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index b0b914b5c..75621995c 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 --*/
 #include<iostream>
+#include"z3_omp.h"
 #include"util.h"
 #include"timeout.h"
 #include"error_codes.h"